diff --git a/.github/workflows/push_main.yml b/.github/workflows/push_main.yml index b2873ec7aa..57f12db989 100644 --- a/.github/workflows/push_main.yml +++ b/.github/workflows/push_main.yml @@ -17,9 +17,6 @@ jobs: if: github.ref == 'refs/heads/main' uses: leanprover-contrib/update-versions-action@master - - uses: satackey/action-docker-layer-caching@v0.0.11 - continue-on-error: true - - name: build docker container run: docker build -t con-nf . diff --git a/src/phase2/approximation.lean b/src/phase2/approximation.lean index dd9612fc87..825207381b 100644 --- a/src/phase2/approximation.lean +++ b/src/phase2/approximation.lean @@ -262,10 +262,6 @@ end extends approximates π₀ π : Prop := (exception_mem : ∀ a, π.is_exception a → a ∈ π₀.atom_perm.domain) -lemma exactly_approximates_of_eq {π₀ π₀' : near_litter_approx} {π : near_litter_perm} - (h : π₀.exactly_approximates π) (h' : π₀ = π₀') : - π₀'.exactly_approximates π := by rwa [h'] at h - lemma exactly_approximates.of_is_exception {π₀ : near_litter_approx} {π : near_litter_perm} (hπ : π₀.exactly_approximates π) (a : atom) (ha : a.1 ∈ π₀.litter_perm.domain) : π.is_exception a → π₀ • a ∉ litter_set (π₀ • a.1) ∨ π₀.symm • a ∉ litter_set (π₀.symm • a.1) := @@ -368,10 +364,6 @@ def approximates {β : type_index} (π₀ : struct_approx β) (π : struct_perm def exactly_approximates {β : type_index} (π₀ : struct_approx β) (π : struct_perm β) : Prop := ∀ A, (π₀ A).exactly_approximates (struct_perm.of_bot $ struct_perm.derivative A π) -lemma exactly_approximates_of_eq {β : type_index} {π₀ π₀' : struct_approx β} {π : struct_perm β} - (h : π₀.exactly_approximates π) (h' : π₀ = π₀') : - π₀'.exactly_approximates π := by rwa [h'] at h - variables {α : Λ} [position_data.{}] [phase_2_assumptions α] /-- A structural approximation `π` *supports* a set of support conditions if all of the support @@ -477,6 +469,24 @@ def comp {β γ : type_index} (π₀ : struct_approx β) (A : path β γ) : stru (A : path β γ) (B : extended_index γ) : π₀.comp A B = π₀ (A.comp B) := rfl +lemma approximates.comp {β γ : type_index} {π₀ : struct_approx β} {π : struct_perm β} + (h : π₀.approximates π) (A : path β γ) : + (π₀.comp A).approximates (struct_perm.derivative A π) := +begin + intros B, + rw [comp_apply, struct_perm.derivative_derivative], + exact h _, +end + +lemma exactly_approximates.comp {β γ : type_index} {π₀ : struct_approx β} {π : struct_perm β} + (h : π₀.exactly_approximates π) (A : path β γ) : + (π₀.comp A).exactly_approximates (struct_perm.derivative A π) := +begin + intros B, + rw [comp_apply, struct_perm.derivative_derivative], + exact h _, +end + /-! # Induction on support conditions -/ diff --git a/src/phase2/complete_action.lean b/src/phase2/complete_action.lean index fed98a3afa..45ef7d711a 100644 --- a/src/phase2/complete_action.lean +++ b/src/phase2/complete_action.lean @@ -647,10 +647,10 @@ begin end def in_out (π : near_litter_perm) (a : atom) (L : litter) : Prop := -xor ((π • a).1 = π • L) (a.1 = L) +xor (a.1 = L) ((π • a).1 = π • L) lemma in_out_def {π : near_litter_perm} {a : atom} {L : litter} : - in_out π a L ↔ xor ((π • a).1 = π • L) (a.1 = L) := iff.rfl + in_out π a L ↔ xor (a.1 = L) ((π • a).1 = π • L) := iff.rfl structure _root_.con_nf.near_litter_perm.biexact (π π' : near_litter_perm) (atoms : set atom) (litters : set litter) : Prop := @@ -724,12 +724,12 @@ begin by_cases h'' : (π'⁻¹ • π • a).1 = L, { refine ⟨_, h'', _⟩, rw smul_inv_smul, }, - { have := h.right_exact L hL _ (or.inl ⟨_, h''⟩), + { have := h.right_exact L hL _ (or.inr ⟨_, h''⟩), { rw [smul_inv_smul, smul_left_cancel_iff, inv_smul_eq_iff] at this, rw this, exact ⟨a, ha, rfl⟩, }, { rw [smul_inv_smul, h', h.smul_eq_smul_litter L hL], }, }, - { rw h.left_exact L hL a (or.inr ⟨ha, h'⟩), + { rw h.left_exact L hL a (or.inl ⟨ha, h'⟩), simp only [litter.coe_to_near_litter, smul_mem_smul_set_iff, mem_litter_set], exact ha, }, end @@ -768,20 +768,20 @@ begin exact ⟨b, hb, rfl⟩, }, end --- `in_out` is just another way to quantify exceptions, focusing on a slightly different litter. --- Basically `in_out` looks only at images not preimages. -example (π : near_litter_perm) (a : atom) (L : litter) : +/- `in_out` is just another way to quantify exceptions, focusing on a slightly different litter. +Basically `in_out` looks only at images not preimages. -/ +lemma is_exception_of_in_out {π : near_litter_perm} {a : atom} {L : litter} : in_out π a L → π.is_exception a ∨ π.is_exception (π • a) := begin - rintro (ha | ⟨rfl, ha⟩), - { refine or.inl (or.inl _), - rw [mem_litter_set, ha.1, smul_left_cancel_iff], - exact ne.symm ha.2, }, + rintro (⟨rfl, ha⟩ | ha), { refine or.inr (or.inr _), intro h, rw [mem_litter_set, eq_inv_smul_iff] at h, rw [← h, inv_smul_smul] at ha, exact ha rfl, }, + { refine or.inl (or.inl _), + rw [mem_litter_set, ha.1, smul_left_cancel_iff], + exact ne.symm ha.2, }, end structure biexact {β : Iio α} (π π' : struct_perm β) (c : support_condition β) : Prop := @@ -791,12 +791,10 @@ structure biexact {β : Iio α} (π π' : struct_perm β) (c : support_condition (smul_eq_smul_litter : ∀ A : extended_index β, ∀ L : litter, (inr L.to_near_litter, A) ≤[α] c → flexible α L A → struct_perm.derivative A π • L = struct_perm.derivative A π' • L) -(left_exact : ∀ A : extended_index β, ∀ L : litter, ∀ a : atom, - (inr L.to_near_litter, A) ≤[α] c → in_out (struct_perm.of_bot $ struct_perm.derivative A π) a L → - struct_perm.derivative A π • a = struct_perm.derivative A π' • a) -(right_exact : ∀ A : extended_index β, ∀ L : litter, ∀ a : atom, - (inr L.to_near_litter, A) ≤[α] c → in_out (struct_perm.of_bot $ struct_perm.derivative A π') a L → - struct_perm.derivative A π • a = struct_perm.derivative A π' • a) +(exact : ∀ A : extended_index β, ∀ L : litter, + (inr L.to_near_litter, A) ≤[α] c → + struct_perm.derivative A π • L = struct_perm.derivative A π' • L → + struct_perm.derivative A π • L.to_near_litter = struct_perm.derivative A π' • L.to_near_litter) lemma biexact.atoms {β : Iio α} {π π' : struct_perm β} {c : support_condition β} (h : biexact π π' c) (A : extended_index β) : @@ -812,8 +810,7 @@ lemma biexact.constrains {β : Iio α} {π π' : struct_perm β} {c d : support_ ⟨ λ A a ha, h.smul_eq_smul_atom A a (ha.trans h'), λ A L hL, h.smul_eq_smul_litter A L (hL.trans h'), - λ A L a hL, h.left_exact A L a (hL.trans h'), - λ A L a hL, h.right_exact A L a (hL.trans h'), + λ A L hL, h.exact A L (hL.trans h'), ⟩ lemma biexact.smul_eq_smul {β : Iio α} {π π' : allowable β} {c : support_condition β} @@ -855,15 +852,7 @@ begin obtain ⟨L, rfl⟩ := hL.exists_litter_eq, suffices : struct_perm.derivative A π.to_struct_perm • L = struct_perm.derivative A π'.to_struct_perm • L, - { have := near_litter_perm.biexact.litter L this _ _, - { refine (this.union (h.atoms A)).smul_near_litter L.to_near_litter (or.inl rfl) _, - intros a ha, - rw [litter.to_near_litter_fst, litter.coe_to_near_litter, symm_diff_self] at ha, - cases ha, }, - { intros a ha, - exact h.left_exact A L a relation.refl_trans_gen.refl ha, }, - { intros a ha, - exact h.right_exact A L a relation.refl_trans_gen.refl ha, }, }, + { exact h.exact _ _ relation.refl_trans_gen.refl this, }, obtain (hL | hL) := flexible_cases α L A, swap, { exact h.smul_eq_smul_litter A L relation.refl_trans_gen.refl hL, }, @@ -930,6 +919,21 @@ begin exact inr_injective this.1, end +lemma mem_dom_of_exactly_approximates {β : Iio α} {π₀ : struct_approx β} + {π : struct_perm β} (hπ : π₀.exactly_approximates π) + {a : atom} {L : litter} {A : extended_index β} + (h : in_out (struct_perm.of_bot $ struct_perm.derivative A π) a L) : + a ∈ (π₀ A).atom_perm.domain := +begin + obtain (h | h) := is_exception_of_in_out h, + { exact (hπ A).exception_mem _ h, }, + { have h₁ := (hπ A).exception_mem _ h, + have := (hπ A).symm_map_atom _ h₁, + rw inv_smul_smul at this, + rw ← this, + exact (π₀ A).atom_perm.symm.map_domain h₁, }, +end + lemma coherent {γ : Iio α} (A : path (β : type_index) γ) (N : near_litter × extended_index γ) (c d : support_condition β) (hc : (inr N.1, A.comp N.2) <[α] c) @@ -1018,7 +1022,9 @@ begin refine struct_action.lawful.comp _ _, refine (hπ.le (struct_action.le_comp (ih_action_le_ihs_action π c d) _)).le _, exact struct_action.le_comp (ih_action_le hc'.to_refl) _, }, - swap, sorry, + swap, + { rw [inflexible_coe.comp_B, ← path.comp_cons], + sorry, }, obtain ⟨δ, ε, ζ, hε, hζ, hεζ, C, t, rfl, rfl⟩ := hL, rw struct_perm.derivative_cons, refine eq.trans _ (struct_perm.derivative_bot_smul _ _).symm, @@ -1128,10 +1134,34 @@ begin simp only [← hNL, path.comp_assoc, ← path.comp_cons], exact trans_gen_constrains_comp hLN _, }, { exact hL₂, }, }, - { intros E L a hL haL, - sorry, }, - { intros E L a hL haL, - sorry, }, }, }, + { intros E L hL₁ hL₂, + have hLN : (inr L.to_near_litter, (C.cons $ coe_lt hε).comp E) <[α] + (inr N.fst.to_near_litter, (C.cons $ coe_lt hζ).cons (bot_lt_coe _)), + { simp only [hNL], + refine relation.trans_gen.tail' _ (constrains.f_map hε _ _ _ _ _ hct), + exact refl_trans_gen_constrains_comp hL₁ _, }, + specialize ih (L.to_near_litter, ((C.cons $ coe_lt hε).comp E)) + (trans_gen_near_litter hLN) + (trans (trans_gen_constrains_comp (trans_gen_near_litter hLN) _) hc), + simp only at ih, + rw [← path.comp_assoc, path.comp_cons] at ih, + refine (near_litter_action.smul_to_near_litter_eq_of_precise_at _ + (struct_action.hypothesised_allowable_exactly_approximates + (ih_action _) ⟨δ, ε, ζ, hε, hζ, hεζ, A.comp C, t, rfl, rfl⟩ _ _ _) + _ (near_litter_action.refine_precise _) _).trans _, + { refine relation.trans_gen.tail' (refl_trans_gen_constrains_comp hL₁ _) _, + exact constrains.f_map _ _ _ _ _ _ hct, }, + { refine hL₂.trans _, + simp only [struct_action.comp_apply, struct_action.refine_apply, + near_litter_action.refine_litter_map, ih_action_litter_map, + foa_hypothesis_near_litter_image], + rw [ih, ← allowable.derivative_to_struct_perm, struct_perm.derivative_derivative], + refl, }, + { simp only [struct_action.comp_apply, struct_action.refine_apply, + near_litter_action.refine_litter_map, ih_action_litter_map, + foa_hypothesis_near_litter_image], + rw [ih, ← allowable.derivative_to_struct_perm, + struct_perm.derivative_derivative], }, }, }, }, end end struct_approx