From b80daa54f1d9dc56060d7f7512c38b9a268bd712 Mon Sep 17 00:00:00 2001 From: zeramorphic Date: Sun, 13 Aug 2023 23:03:02 +0100 Subject: [PATCH] Structure of surjectivity for FoA Signed-off-by: zeramorphic --- src/phase2/complete_action.lean | 99 ++++++++++++++++++++++++++++----- 1 file changed, 84 insertions(+), 15 deletions(-) diff --git a/src/phase2/complete_action.lean b/src/phase2/complete_action.lean index 03e5645b27..7b60f8d559 100644 --- a/src/phase2/complete_action.lean +++ b/src/phase2/complete_action.lean @@ -1032,19 +1032,19 @@ lemma complete_litter_map_inflexible_coe_iff (hπf : π.free) {c d : support_con ⟩ lemma ihs_action_coherent_precise' (hπf : π.free) {γ : Iio α} (A : path (β : type_index) γ) - (N : near_litter × extended_index γ) - (c d : support_condition β) (hc : (inr N.1, A.comp N.2) <[α] c) + (N : extended_index γ × near_litter) + (c d : support_condition β) (hc : (inr N.2, A.comp N.1) <[α] c) (hπ : ((ihs_action π c d).comp A).lawful) (ρ : allowable γ) (h : (((ihs_action π c d).comp A).rc hπ).exactly_approximates ρ.to_struct_perm) : - complete_near_litter_map π (A.comp N.2) N.1 = struct_perm.derivative N.2 ρ.to_struct_perm • N.1 := + complete_near_litter_map π (A.comp N.1) N.2 = struct_perm.derivative N.1 ρ.to_struct_perm • N.2 := begin revert hc, refine well_founded.induction (inv_image.wf _ (relation.trans_gen.is_well_founded (constrains α γ)).wf) N _, - exact λ N : near_litter × extended_index γ, (inr N.1, N.2), + exact λ N : extended_index γ × near_litter, (inr N.2, N.1), clear N, - rintros ⟨N, B⟩ ih hc, + rintros ⟨B, N⟩ ih hc, dsimp only at *, have hdom : ((((ihs_action π c d).comp A B).refine (hπ B)).litter_map N.fst).dom := or.inl (trans_gen_near_litter' hc), @@ -1217,7 +1217,7 @@ begin 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], - specialize ih (L.to_near_litter, (C.cons $ coe_lt hε).comp E) (trans_gen_near_litter hLN) + specialize ih ((C.cons $ coe_lt hε).comp E, L.to_near_litter) (trans_gen_near_litter hLN) (trans (trans_gen_constrains_comp (trans_gen_near_litter hLN) _) hc), { dsimp only at ih, rw [← path.comp_assoc, path.comp_cons] at ih, @@ -1237,7 +1237,7 @@ begin { 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)) + specialize ih (((C.cons $ coe_lt hε).comp E), L.to_near_litter) (trans_gen_near_litter hLN) (trans (trans_gen_constrains_comp (trans_gen_near_litter hLN) _) hc), simp only at ih, @@ -1273,7 +1273,7 @@ lemma ihs_action_coherent_precise (hπf : π.free) {γ : Iio α} (A : path (β : (ρ : allowable γ) (h : (((ihs_action π c d).comp A).rc hπ).exactly_approximates ρ.to_struct_perm) : complete_near_litter_map π (A.comp B) N = struct_perm.derivative B ρ.to_struct_perm • N := -ihs_action_coherent_precise' hπf A (N, B) c d hc hπ ρ h +ihs_action_coherent_precise' hπf A (B, N) c d hc hπ ρ h /-- The coherence lemma for atoms, which is much easier to prove. @@ -1975,6 +1975,15 @@ noncomputable def preimage_action (hπf : π.free) (c : support_condition β) : end, } +@[simp] lemma preimage_action_atom_map_dom {hπf : π.free} {c : support_condition β} + {B : extended_index β} {a : atom} : + ((preimage_action hπf c B).atom_map a).dom ↔ (inl (π.complete_atom_map B a), B) <[α] c := iff.rfl + +@[simp] lemma preimage_action_litter_map_dom {hπf : π.free} {c : support_condition β} + {B : extended_index β} {L : litter} : + ((preimage_action hπf c B).litter_map L).dom ↔ + (inr (π.complete_near_litter_map B L.to_near_litter), B) <[α] c := iff.rfl + lemma preimage_action_lawful {hπf : π.free} {c : support_condition β} : (preimage_action hπf c).lawful := begin @@ -2034,10 +2043,33 @@ end lemma _root_.relation.refl_trans_gen_of_eq {α : Type*} {r : α → α → Prop} {x y : α} (h : x = y) : relation.refl_trans_gen r x y := by cases h; refl +lemma preimage_action_coherent_precise (hπf : π.free) {γ : Iio α} (A : path (β : type_index) γ) + (B : extended_index γ) (N : near_litter) + (c : support_condition β) (hc : (inr (π.complete_near_litter_map (A.comp B) N), A.comp B) <[α] c) + (ρ : allowable γ) + (h : (((preimage_action hπf c).comp A).rc (preimage_action_lawful.comp _)).exactly_approximates + ρ.to_struct_perm) : + complete_near_litter_map π (A.comp B) N = struct_perm.derivative B ρ.to_struct_perm • N := +sorry + +lemma preimage_action_coherent_precise_atom (hπf : π.free) {γ : Iio α} (A : path (β : type_index) γ) + (B : extended_index γ) (a : atom) + (c : support_condition β) (hc : (inl (π.complete_atom_map (A.comp B) a), A.comp B) <[α] c) + (ρ : allowable γ) + (h : (((preimage_action hπf c).comp A).rc (preimage_action_lawful.comp _)).exactly_approximates + ρ.to_struct_perm) : + complete_atom_map π (A.comp B) a = struct_perm.derivative B ρ.to_struct_perm • a := +begin + refine eq.trans _ ((h B).map_atom a (or.inl (or.inl (or.inl (or.inl hc))))), + rw struct_action.rc_smul_atom_eq, + refl, + exact hc, +end + lemma complete_litter_map_surjective_extends (hπf : π.free) (A : extended_index β) (L : litter) - (ha : ∀ B (a : atom), (inl a, B) <[α] (inr L.to_near_litter, A) → + (ha : ∀ B (a : atom), (inl a, B) ≺[α] (inr L.to_near_litter, A) → a ∈ range (π.complete_atom_map B)) - (hN : ∀ B N, (inr N, B) <[α] (inr L.to_near_litter, A) → + (hN : ∀ B N, (inr N, B) ≺[α] (inr L.to_near_litter, A) → N ∈ range (π.complete_near_litter_map B)) : L ∈ range (π.complete_litter_map A) := begin @@ -2048,7 +2080,7 @@ begin exact h, }, { exact near_litter_approx.flexible_completion_symm_smul_flexible α (π A) A (hπf A) L h, }, }, { obtain ⟨γ, ε, hε, C, a, rfl, rfl⟩ := h, - obtain ⟨b, rfl⟩ := ha _ a (relation.trans_gen.single $ constrains.f_map_bot hε _ a), + obtain ⟨b, rfl⟩ := ha _ a (constrains.f_map_bot hε _ a), refine ⟨f_map (show ⊥ ≠ (ε : type_index), from bot_ne_coe) b, _⟩, rw complete_litter_map_eq_of_inflexible_bot ⟨γ, ε, hε, C, b, rfl, rfl⟩, }, { obtain ⟨γ, δ, ε, hδ, hε, hδε, B, t, rfl, rfl⟩ := h, @@ -2069,7 +2101,7 @@ begin { refine prod.ext _ rfl, change inl _ = inl _, simp only, - have hac := relation.trans_gen.single (constrains.f_map hδ _ _ _ _ _ hc), + have hac := constrains.f_map hδ _ _ _ _ _ hc, specialize ha _ a hac, obtain ⟨b, ha⟩ := ha, have : (struct_perm.derivative A @@ -2079,7 +2111,11 @@ begin (preimage_action_lawful.comp _) (preimage_action_comp_map_flexible _)).to_struct_perm)⁻¹ • a = b, { rw [inv_smul_eq_iff, ← ha], - sorry, }, + rw struct_action.hypothesised_allowable, + refine preimage_action_coherent_precise_atom hπf (B.cons $ coe_lt hδ) A b _ _ _ + (struct_action.allowable_exactly_approximates _ _ _ _), + rw ha, + exact relation.trans_gen.single hac, }, transitivity b, { rw [map_inv, map_inv, this], }, { rw [map_inv, map_inv, ← smul_eq_iff_eq_inv_smul, ← ha], @@ -2096,7 +2132,7 @@ begin { refine prod.ext _ rfl, change inr _ = inr _, simp only, - have hNc := relation.trans_gen.single (constrains.f_map hδ _ _ _ _ _ hc), + have hNc := constrains.f_map hδ _ _ _ _ _ hc, specialize hN _ N hNc, obtain ⟨N', hN⟩ := hN, have : (struct_perm.derivative A @@ -2106,7 +2142,11 @@ begin (preimage_action_lawful.comp _) (preimage_action_comp_map_flexible _)).to_struct_perm)⁻¹ • N = N', { rw [inv_smul_eq_iff, ← hN], - sorry, }, + rw struct_action.hypothesised_allowable, + refine preimage_action_coherent_precise hπf (B.cons $ coe_lt hδ) A N' _ _ _ + (struct_action.allowable_exactly_approximates _ _ _ _), + rw hN, + exact relation.trans_gen.single hNc, }, transitivity N', { rw [map_inv, map_inv, this], }, { rw [map_inv, map_inv, ← smul_eq_iff_eq_inv_smul, ← hN], @@ -2122,6 +2162,35 @@ begin simp only [map_inv, eq_inv_smul_iff, ← this, smul_inv_smul], }, }, }, end +lemma complete_near_litter_map_surjective_extends (hπf : π.free) (A : extended_index β) + (N : near_litter) (hL : N.1 ∈ range (π.complete_litter_map A)) + (ha : litter_set N.1 ∆ N ⊆ range (π.complete_atom_map A)) : + N ∈ range (π.complete_near_litter_map A) := sorry + +variable (π) + +def complete_map_surjective_at : support_condition β → Prop +| (inl a, A) := a ∈ range (π.complete_atom_map A) +| (inr N, A) := N ∈ range (π.complete_near_litter_map A) + +variable {π} + +lemma complete_map_surjective_extends (hπf : π.free) (c : support_condition β) + (hc : ∀ d : support_condition β, d ≺[α] c → π.complete_map_surjective_at d) : + π.complete_map_surjective_at c := sorry + +lemma complete_map_surjective_at_all (hπf : π.free) (c : support_condition β) : + π.complete_map_surjective_at c := sorry + +lemma complete_atom_map_surjective (hπf : π.free) (A : extended_index β) : + surjective (π.complete_atom_map A) := sorry + +lemma complete_near_litter_map_surjective (hπf : π.free) (A : extended_index β) : + surjective (π.complete_near_litter_map A) := sorry + +lemma complete_litter_map_surjective (hπf : π.free) (A : extended_index β) : + surjective (π.complete_litter_map A) := sorry + end struct_approx end con_nf