Skip to content

Commit

Permalink
Bump mathlib, revert FoA break
Browse files Browse the repository at this point in the history
  • Loading branch information
zeramorphic committed Nov 15, 2023
1 parent e9cb041 commit 687862a
Show file tree
Hide file tree
Showing 5 changed files with 36 additions and 88 deletions.
10 changes: 7 additions & 3 deletions ConNF/Foa/Basic/Hypotheses.lean
Original file line number Diff line number Diff line change
Expand Up @@ -130,9 +130,7 @@ class FoaAssumptions extends FoaData α where
Allowable.toStructPerm (allowableCons β γ hγ ρ)
/-- Designated supports commute with allowable permutations. -/
smul_designatedSupport {β : Iic α} (t : Tangle β) (ρ : Allowable β) :
∃ ρ' : Allowable β, ρ' • t = ρ • t ∧
∀ c : SupportCondition β,
c ∈ designatedSupport t ↔ ρ' • c ∈ designatedSupport (ρ' • t)
ρ • (designatedSupport t : Set (SupportCondition β)) = designatedSupport (ρ • t)
/-- The `fuzz` map commutes with allowable permutations. -/
smul_fuzz {β : IicBot α} (γ : IioBot α) (δ : Iio α) (hγ : (γ : TypeIndex) < β)
(hδ : (δ : TypeIndex) < β) (hγδ : γ ≠ δ) (ρ : Allowable β) (t : Tangle γ) :
Expand Down Expand Up @@ -249,6 +247,12 @@ theorem Allowable.comp_bot {β : IicBot α}
change NearLitterPerm.ofBot (Allowable.comp A ρ) • a = Allowable.toStructPerm ρ A • a
simp only [Allowable.toStructPerm_apply]

theorem smul_mem_designatedSupport {β : Iio α} {c : SupportCondition β} {t : Tangle β}
(h : c ∈ designatedSupport t) (π : Allowable β) : π • c ∈ designatedSupport (π • t) :=
(Set.ext_iff.mp (smul_designatedSupport (show Tangle (β : Iic α) from t) π)
((show Allowable (β : Iic α) from π) • c)).mp
⟨c, h, rfl⟩

@[simp]
theorem ofBot_comp' {β : IicBot α} {hβ : ⊥ < β} {ρ : Allowable β} :
NearLitterPerm.ofBot (allowableCons β ⊥ hβ ρ) =
Expand Down
76 changes: 10 additions & 66 deletions ConNF/Foa/Properties/Surjective.lean
Original file line number Diff line number Diff line change
Expand Up @@ -138,62 +138,6 @@ theorem preimageAction_coherent_atom (hπf : π.Free) {γ : Iio α} (A : Path (
refine' ⟨_, _, Relation.ReflTransGen.refl⟩
exact hc

theorem completeLitterMap_surjective_extends_inflexibleCoe (hπf : π.Free) (A : ExtendedIndex β)
(P : InflexibleCoePath A) (t : Tangle P.δ)
(ha : ∀ (B : ExtendedIndex β) (a : Atom),
⟨B, inl a⟩ ≺[α] ⟨A, inr (fuzz (coe_ne_coe.mpr <| coe_ne' P.hδε) t).toNearLitter⟩ →
a ∈ range (π.completeAtomMap B))
(hN : ∀ (B : ExtendedIndex β) (N : NearLitter),
⟨B, inr N⟩ ≺[α] ⟨A, inr (fuzz (coe_ne_coe.mpr <| coe_ne' P.hδε) t).toNearLitter⟩ →
N ∈ range (π.completeNearLitterMap B)) :
fuzz (coe_ne_coe.mpr <| coe_ne' P.hδε) t ∈ range (completeLitterMap π A) := by
obtain ⟨ρ, hρ₁, hρ₂⟩ := smul_designatedSupport t
((preimageAction hπf
⟨(P.B.cons (coe_lt P.hε)).cons (bot_lt_coe _),
inr (fuzz (coe_ne_coe.mpr <| coe_ne' P.hδε) t).toNearLitter⟩).hypothesisedAllowable
P ((preimageAction_lawful hπf).comp _) (preimageAction_comp_mapFlexible _))⁻¹
refine ⟨fuzz (coe_ne_coe.mpr <| coe_ne' P.hδε) (ρ • t), ?_⟩
rw [completeLitterMap_eq_of_inflexibleCoe ⟨P, _, rfl⟩
((ihAction_lawful hπf _).comp _) (ihAction_comp_mapFlexible hπf _ _)]
refine' congr_arg _ _
dsimp only
obtain ⟨γ, δ, ε, hδ, hε, hδε, B, rfl⟩ := P
rw [smul_eq_iff_eq_inv_smul, hρ₁]
refine supports (t := t) ?_ ?_
· intros A a hc
have hac := Constrains.fuzz hδ hε hδε B t _ hc
specialize ha _ a hac
obtain ⟨b, ha⟩ := ha
have : (Tree.comp A
(Allowable.toStructPerm ((preimageAction hπf
⟨(B.cons (coe_lt hε)).cons (bot_lt_coe _),
inr (fuzz (coe_ne_coe.mpr <| coe_ne' hδε) t).toNearLitter⟩).hypothesisedAllowable
⟨γ, δ, ε, hδ, hε, hδε, B, rfl⟩ ((preimageAction_lawful hπf).comp _)
(preimageAction_comp_mapFlexible _))))⁻¹ • a = b
· rw [inv_smul_eq_iff, ← ha]
rw [StructAction.hypothesisedAllowable]
refine' preimageAction_coherent_atom hπf (B.cons <| coe_lt hδ) A b _ _ _
(StructAction.allowable_exactlyApproximates _ _ _ _)
rw [ha]
exact hac
trans b
· rw [map_inv]
exact this
· rw [map_inv, Tree.inv_apply, ← smul_eq_iff_eq_inv_smul, ← ha]
rw [StructAction.hypothesisedAllowable]
refine' (ihAction_coherent_atom (B.cons <| coe_lt hδ) A b _ _
((ihAction_lawful hπf _).comp _) _
(StructAction.allowable_exactlyApproximates _ _ _ _)).symm
have hρ₂' := (hρ₂ ⟨A, inl a⟩).mp hc
rw [hρ₁] at hρ₂'
refine' Relation.TransGen.tail' _ (Constrains.fuzz hδ hε hδε B _ _ hρ₂')
refine' Relation.reflTransGen_of_eq _
refine' SupportCondition.ext _ _ rfl _
change inl _ = inl _
simp only [← this, Tree.comp_bot, Tree.toBot_inv_smul, inl.injEq]
sorry
· sorry

theorem completeLitterMap_surjective_extends (hπf : π.Free) (A : ExtendedIndex β) (L : Litter)
(ha : ∀ (B : ExtendedIndex β) (a : Atom),
⟨B, inl a⟩ ≺[α] ⟨A, inr L.toNearLitter⟩ → a ∈ range (π.completeAtomMap B))
Expand All @@ -210,19 +154,19 @@ theorem completeLitterMap_surjective_extends (hπf : π.Free) (A : ExtendedIndex
obtain ⟨b, rfl⟩ := ha _ a (Constrains.fuzz_bot hε _ a)
refine' ⟨fuzz (show ⊥ ≠ (ε : TypeIndex) from bot_ne_coe) b, _⟩
rw [completeLitterMap_eq_of_inflexibleBot ⟨⟨γ, ε, hε, C, rfl⟩, b, rfl⟩]
· obtain ⟨P, t, rfl⟩ := h
exact completeLitterMap_surjective_extends_inflexibleCoe hπf A P t ha hN
/- refine' ⟨fuzz (coe_ne_coe.mpr <| coe_ne' P.hδε)
· obtain ⟨⟨γ, δ, ε, hδ, hε, hδε, B, rfl⟩, t, rfl⟩ := h
refine' ⟨fuzz (coe_ne_coe.mpr <| coe_ne' hδε)
(((preimageAction hπf
⟨(P.B.cons (coe_lt P.hε)).cons (bot_lt_coe _),
inr (fuzz (coe_ne_coe.mpr <| coe_ne' P.hδε) t).toNearLitter⟩).hypothesisedAllowable
P ((preimageAction_lawful hπf).comp _) (preimageAction_comp_mapFlexible _))⁻¹ • t), _⟩
rw [completeLitterMap_eq_of_inflexibleCoe ⟨P, _, rfl⟩
⟨(B.cons (coe_lt hε)).cons (bot_lt_coe _),
inr (fuzz (coe_ne_coe.mpr <| coe_ne' hδε) t).toNearLitter⟩).hypothesisedAllowable
⟨γ, δ, ε, hδ, hε, hδε, B, rfl⟩
((preimageAction_lawful hπf).comp _) (preimageAction_comp_mapFlexible _))⁻¹ • t), _⟩
rw [completeLitterMap_eq_of_inflexibleCoe ⟨⟨γ, δ, ε, hδ, hε, hδε, B, rfl⟩, _, rfl⟩
((ihAction_lawful hπf _).comp _) (ihAction_comp_mapFlexible hπf _ _)]
refine' congr_arg _ _
dsimp only
rw [smul_eq_iff_eq_inv_smul] -/
/- refine supports (t := t) ?_ ?_
rw [smul_eq_iff_eq_inv_smul]
refine supports (t := t) ?_ ?_
· intros A a hc
have hac := Constrains.fuzz hδ hε hδε B t _ hc
specialize ha _ a hac
Expand Down Expand Up @@ -284,7 +228,7 @@ theorem completeLitterMap_surjective_extends (hπf : π.Free) (A : ExtendedIndex
refine' SupportCondition.ext _ _ rfl _
change inr _ = inr _
simp only [← this, ne_eq, Tree.comp_bot, Tree.toBot_inv_smul, map_inv,
Tree.inv_apply] -/
Tree.inv_apply]

theorem atom_mem_range_of_mem_completeNearLitterMap (A : ExtendedIndex β) (a : Atom)
{N : NearLitter} (h : a ∈ π.completeNearLitterMap A N) : a ∈ range (π.completeAtomMap A) := by
Expand Down
36 changes: 18 additions & 18 deletions lake-manifest.json
Original file line number Diff line number Diff line change
Expand Up @@ -4,59 +4,59 @@
[{"git":
{"url": "https://github.com/leanprover-community/mathlib4.git",
"subDir?": null,
"rev": "6b83e01c4b771afdf9316fbc69269a7560b12b67",
"rev": "0b128365295bc885cae8a0571405eafee1368247",
"opts": {},
"name": "mathlib",
"inputRev?": null,
"inherited": false}},
{"git":
{"url": "https://github.com/leanprover/doc-gen4",
"subDir?": null,
"rev": "8bccb92b531248af1b6692d65486e8640c8bcd10",
"rev": "96147eaa0c066a95210fe5518c987e77be034b9f",
"opts": {},
"name": "«doc-gen4»",
"inputRev?": "main",
"inherited": false}},
{"git":
{"url": "https://github.com/leanprover-community/quote4",
"subDir?": null,
"rev": "a387c0eb611857e2460cf97a8e861c944286e6b2",
"rev": "d3a1d25f3eba0d93a58d5d3d027ffa78ece07755",
"opts": {},
"name": "Qq",
"inputRev?": "master",
"inherited": true}},
{"git":
{"url": "https://github.com/leanprover-community/aesop",
"subDir?": null,
"rev": "bf5ab42a58e71de7ebad399ce3f90d29aae7fca9",
"opts": {},
"name": "aesop",
"inputRev?": "master",
"inherited": true}},
{"git":
{"url": "https://github.com/leanprover/lean4-cli",
"subDir?": null,
"rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa",
"rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
"opts": {},
"name": "Cli",
"inputRev?": "nightly",
"inputRev?": "main",
"inherited": true}},
{"git":
{"url": "https://github.com/leanprover-community/ProofWidgets4",
"subDir?": null,
"rev": "f1a5c7808b001305ba07d8626f45ee054282f589",
"rev": "c3b9f0d4ebedc43635d3f7e764e277b1010844b7",
"opts": {},
"name": "proofwidgets",
"inputRev?": "v0.0.21",
"inputRev?": "v0.0.22",
"inherited": true}},
{"git":
{"url": "https://github.com/leanprover/std4",
"subDir?": null,
"rev": "6747f41f28627bed83e6d5891683538211caa2c1",
"rev": "c14f6a65b2c08caa38e1ab5db83451460d6cde3e",
"opts": {},
"name": "std",
"inputRev?": "main",
"inherited": true}},
{"git":
{"url": "https://github.com/leanprover-community/aesop",
"subDir?": null,
"rev": "6749fa4e776919514dae85bfc0ad62a511bc42a7",
"opts": {},
"name": "aesop",
"inputRev?": "master",
"inherited": true}},
{"git":
{"url": "https://github.com/xubaiw/CMark.lean",
"subDir?": null,
Expand All @@ -68,9 +68,9 @@
{"git":
{"url": "https://github.com/fgdorais/lean4-unicode-basic",
"subDir?": null,
"rev": "f09250282cea3ed8c010f430264d9e8e50d7bc32",
"rev": "4ecf4f1f98d14d03a9e84fa1c082630fa69df88b",
"opts": {},
"name": "«lean4-unicode-basic»",
"name": "UnicodeBasic",
"inputRev?": "main",
"inherited": true}},
{"git":
Expand Down
2 changes: 1 addition & 1 deletion lean-toolchain
Original file line number Diff line number Diff line change
@@ -1 +1 @@
leanprover/lean4:v4.2.0-rc4
leanprover/lean4:v4.3.0-rc1
Empty file modified update_mathlib.sh
100644 → 100755
Empty file.

0 comments on commit 687862a

Please sign in to comment.