Skip to content

Commit

Permalink
update v.15.0-rc1 (#175)
Browse files Browse the repository at this point in the history
  • Loading branch information
@iehality
iehality authored Dec 12, 2024
1 parent 9033902 commit d5a5b56
Show file tree
Hide file tree
Showing 6 changed files with 142 additions and 142 deletions.
56 changes: 28 additions & 28 deletions Foundation/FirstOrder/Arith/Representation.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,14 +8,14 @@ lemma unit_dom_iff (x : Part Unit) : x.Dom ↔ () ∈ x := by simp [dom_iff_mem,

end Part

namespace Mathlib.Vector
namespace Mathlib.Mathlib.Vector

variable {α : Type*}

lemma cons_get (a : α) (v : Vector α k) : (a ::ᵥ v).get = a :> v.get := by
lemma cons_get (a : α) (v : Mathlib.Vector α k) : (a ::ᵥ v).get = a :> v.get := by
ext i; cases i using Fin.cases <;> simp

end Mathlib.Vector
end Mathlib.Mathlib.Vector

open Encodable Denumerable

Expand Down Expand Up @@ -156,7 +156,7 @@ open Mathlib Encodable Semiterm.Operator.GoedelNumber

section

lemma term_primrec {k f} : (t : Semiterm ℒₒᵣ ξ k) → Primrec (fun v : Vector ℕ k ↦ t.valm ℕ v.get f)
lemma term_primrec {k f} : (t : Semiterm ℒₒᵣ ξ k) → Primrec (fun v : Mathlib.Vector ℕ k ↦ t.valm ℕ v.get f)
| #x => by simpa using Primrec.vector_get.comp .id (.const _)
| &x => by simpa using Primrec.const _
| Semiterm.func Language.Zero.zero _ => by simpa using Primrec.const 0
Expand All @@ -167,32 +167,32 @@ lemma term_primrec {k f} : (t : Semiterm ℒₒᵣ ξ k) → Primrec (fun v : Ve
simpa [Semiterm.val_func] using Primrec.nat_mul.comp (term_primrec (v 0)) (term_primrec (v 1))

lemma sigma1_re (ε : ξ → ℕ) {k} {φ : Semiformula ℒₒᵣ ξ k} (hp : Hierarchy 𝚺 1 φ) :
RePred fun v : Vector ℕ k ↦ Semiformula.Evalm ℕ v.get ε φ := by
RePred fun v : Mathlib.Vector ℕ k ↦ Semiformula.Evalm ℕ v.get ε φ := by
apply sigma₁_induction' hp
case hVerum => simp
case hFalsum => simp
case hEQ =>
intro n t₁ t₂
refine ComputablePred.to_re <| ComputablePred.computable_iff.mpr
<| ⟨fun v : Vector ℕ n ↦ decide (t₁.valm ℕ v.get ε = t₂.valm ℕ v.get ε), ?_, ?_⟩
<| ⟨fun v : Mathlib.Vector ℕ n ↦ decide (t₁.valm ℕ v.get ε = t₂.valm ℕ v.get ε), ?_, ?_⟩
· apply Primrec.to_comp <| Primrec.eq.comp (term_primrec t₁) (term_primrec t₂)
· simp
case hNEQ =>
intro n t₁ t₂
refine ComputablePred.to_re <| ComputablePred.computable_iff.mpr
<| ⟨fun v : Vector ℕ n ↦ !decide (t₁.valm ℕ v.get ε = t₂.valm ℕ v.get ε), ?_, ?_⟩
<| ⟨fun v : Mathlib.Vector ℕ n ↦ !decide (t₁.valm ℕ v.get ε = t₂.valm ℕ v.get ε), ?_, ?_⟩
· apply Primrec.to_comp <| Primrec.not.comp <| Primrec.eq.comp (term_primrec t₁) (term_primrec t₂)
· simp
case hLT =>
intro n t₁ t₂
refine ComputablePred.to_re <| ComputablePred.computable_iff.mpr
<| ⟨fun v : Vector ℕ n ↦ decide (t₁.valm ℕ v.get ε < t₂.valm ℕ v.get ε), ?_, ?_⟩
<| ⟨fun v : Mathlib.Vector ℕ n ↦ decide (t₁.valm ℕ v.get ε < t₂.valm ℕ v.get ε), ?_, ?_⟩
· apply Primrec.to_comp <| Primrec.nat_lt.comp (term_primrec t₁) (term_primrec t₂)
· simp
case hNLT =>
intro n t₁ t₂
refine ComputablePred.to_re <| ComputablePred.computable_iff.mpr
<| ⟨fun v : Vector ℕ n ↦ !decide (t₁.valm ℕ v.get ε < t₂.valm ℕ v.get ε), ?_, ?_⟩
<| ⟨fun v : Mathlib.Vector ℕ n ↦ !decide (t₁.valm ℕ v.get ε < t₂.valm ℕ v.get ε), ?_, ?_⟩
· apply Primrec.to_comp <| Primrec.not.comp <| Primrec.nat_lt.comp (term_primrec t₁) (term_primrec t₂)
· simp
case hAnd =>
Expand All @@ -204,7 +204,7 @@ lemma sigma1_re (ε : ξ → ℕ) {k} {φ : Semiformula ℒₒᵣ ξ k} (hp : Hi
case hBall =>
intro n t φ _ ih
rcases RePred.iff'.mp ih with ⟨f, hf, H⟩
let g : Vector ℕ n →. Unit := fun v ↦
let g : Mathlib.Vector ℕ n →. Unit := fun v ↦
Nat.rec (.some ()) (fun x ih ↦ ih.bind fun _ ↦ f (x ::ᵥ v)) (t.valm ℕ v.get ε)
have : Partrec g :=
Partrec.nat_rec (term_primrec t).to_comp (Computable.const ())
Expand All @@ -220,16 +220,16 @@ lemma sigma1_re (ε : ξ → ℕ) {k} {φ : Semiformula ℒₒᵣ ξ k} (hp : Hi
constructor
· intro h
exact ⟨fun x hx ↦ h x (lt_trans hx (by simp)),
(H (k ::ᵥ v)).mp (by simpa [Vector.cons_get] using h k (by simp))⟩
(H (k ::ᵥ v)).mp (by simpa [Mathlib.Vector.cons_get] using h k (by simp))⟩
· rintro ⟨hs, hd⟩ x hx
rcases lt_or_eq_of_le (Nat.le_of_lt_succ hx) with (hx | rfl)
· exact hs x hx
· simpa [Vector.cons_get] using (H (x ::ᵥ v)).mpr hd
· simpa [Mathlib.Vector.cons_get] using (H (x ::ᵥ v)).mpr hd
case hEx =>
intro n φ _ ih
rcases RePred.iff'.mp ih with ⟨f, _, _⟩
have : RePred fun vx : Vector ℕ n × ℕ ↦ Semiformula.Evalm ℕ (vx.2 :> vx.1.get) ε φ := by
simpa [Vector.cons_get] using ih.comp (Primrec.to_comp <| Primrec.vector_cons.comp .snd .fst)
have : RePred fun vx : Mathlib.Vector ℕ n × ℕ ↦ Semiformula.Evalm ℕ (vx.2 :> vx.1.get) ε φ := by
simpa [Mathlib.Vector.cons_get] using ih.comp (Primrec.to_comp <| Primrec.vector_cons.comp .snd .fst)
simpa using this.projection

end
Expand Down Expand Up @@ -313,8 +313,8 @@ private lemma codeAux_sigma_one {k} (c : Nat.ArithPart₁.Code k) : Hierarchy

@[simp] lemma natCast_nat (n : ℕ) : Nat.cast n = n := by rfl

private lemma models_codeAux {c : Code k} {f : Vector ℕ k →. ℕ} (hc : c.eval f) (y : ℕ) (v : Fin k → ℕ) :
Semiformula.Evalfm ℕ (y :> v) (codeAux c) ↔ f (Vector.ofFn v) = Part.some y := by
private lemma models_codeAux {c : Code k} {f : Mathlib.Vector ℕ k →. ℕ} (hc : c.eval f) (y : ℕ) (v : Fin k → ℕ) :
Semiformula.Evalfm ℕ (y :> v) (codeAux c) ↔ f (Mathlib.Vector.ofFn v) = Part.some y := by
induction hc generalizing y <;> simp [code, codeAux, models_iff]
case zero =>
have : (0 : Part ℕ) = Part.some 0 := rfl
Expand All @@ -334,33 +334,33 @@ private lemma models_codeAux {c : Code k} {f : Vector ℕ k →. ℕ} (hc : c.ev
simp [Semiformula.eval_rew, Function.comp_def, Matrix.empty_eq, Matrix.comp_vecCons']
constructor
· rintro ⟨e, hf, hg⟩
have hf : f (Vector.ofFn e) = Part.some y := (ihf _ _).mp hf
have hg : ∀ i, g i (Vector.ofFn v) = Part.some (e i) := fun i => (ihg i _ _).mp (hg i)
have hf : f (Mathlib.Vector.ofFn e) = Part.some y := (ihf _ _).mp hf
have hg : ∀ i, g i (Mathlib.Vector.ofFn v) = Part.some (e i) := fun i => (ihg i _ _).mp (hg i)
simp [hg, hf]
· intro h
have : ∃ w, (∀ i, Vector.get w i ∈ g i (Vector.ofFn v)) ∧ y ∈ f w := by
have : ∃ w, (∀ i, Mathlib.Vector.get w i ∈ g i (Mathlib.Vector.ofFn v)) ∧ y ∈ f w := by
simpa using Part.eq_some_iff.mp h
rcases this with ⟨w, hw, hy⟩
exact ⟨w.get, (ihf y w.get).mpr (by simpa[Part.eq_some_iff] using hy),
fun i => (ihg i (w.get i) v).mpr (by simpa[Part.eq_some_iff] using hw i)⟩
case rfind c f _ ihf =>
simp [Semiformula.eval_rew, Function.comp_def, Matrix.empty_eq, Matrix.comp_vecCons', ihf, Vector.ofFn_vecCons]
simp [Semiformula.eval_rew, Function.comp_def, Matrix.empty_eq, Matrix.comp_vecCons', ihf, Mathlib.Vector.ofFn_vecCons]
constructor
· rintro ⟨hy, h⟩; simp [Part.eq_some_iff]
exact ⟨by simpa using hy, by intro z hz; exact Nat.not_eq_zero_of_lt (h z hz)⟩
· intro h; simpa [pos_iff_ne_zero] using Nat.mem_rfind.mp (Part.eq_some_iff.mp h)

lemma models_code {c : Code k} {f : Vector ℕ k →. ℕ} (hc : c.eval f) (y : ℕ) (v : Fin k → ℕ) :
Semiformula.Evalbm ℕ (y :> v) (code c) ↔ y ∈ f (Vector.ofFn v) := by
lemma models_code {c : Code k} {f : Mathlib.Vector ℕ k →. ℕ} (hc : c.eval f) (y : ℕ) (v : Fin k → ℕ) :
Semiformula.Evalbm ℕ (y :> v) (code c) ↔ y ∈ f (Mathlib.Vector.ofFn v) := by
simpa[code, models_iff, Semiformula.eval_rew, Matrix.empty_eq, Function.comp_def,
Matrix.comp_vecCons', ←Part.eq_some_iff] using models_codeAux hc y v

noncomputable def codeOfPartrec' {k} (f : Vector ℕ k →. ℕ) : Semisentence ℒₒᵣ (k + 1) :=
code <| Classical.epsilon (fun c ↦ ∀ y v, Semiformula.Evalbm ℕ (y :> v) (code c) ↔ y ∈ f (Vector.ofFn v))
noncomputable def codeOfPartrec' {k} (f : Mathlib.Vector ℕ k →. ℕ) : Semisentence ℒₒᵣ (k + 1) :=
code <| Classical.epsilon (fun c ↦ ∀ y v, Semiformula.Evalbm ℕ (y :> v) (code c) ↔ y ∈ f (Mathlib.Vector.ofFn v))

lemma codeOfPartrec'_spec {k} {f : Vector ℕ k →. ℕ} (hf : Nat.Partrec' f) {y : ℕ} {v : Fin k → ℕ} :
ℕ ⊧/(y :> v) (codeOfPartrec' f) ↔ y ∈ f (Vector.ofFn v) := by
have : ∃ c, ∀ y v, Semiformula.Evalbm ℕ (y :> v) (code c) ↔ y ∈ f (Vector.ofFn v) := by
lemma codeOfPartrec'_spec {k} {f : Mathlib.Vector ℕ k →. ℕ} (hf : Nat.Partrec' f) {y : ℕ} {v : Fin k → ℕ} :
ℕ ⊧/(y :> v) (codeOfPartrec' f) ↔ y ∈ f (Mathlib.Vector.ofFn v) := by
have : ∃ c, ∀ y v, Semiformula.Evalbm ℕ (y :> v) (code c) ↔ y ∈ f (Mathlib.Vector.ofFn v) := by
rcases Nat.ArithPart₁.exists_code (of_partrec hf) with ⟨c, hc⟩
exact ⟨c, models_code hc⟩
exact Classical.epsilon_spec this y v
Expand All @@ -375,7 +375,7 @@ lemma codeOfRePred_spec {p : ℕ → Prop} (hp : RePred p) {x : ℕ} :
ℕ ⊧/![x] (codeOfRePred p) ↔ p x := by
let f : ℕ →. Unit := fun a ↦ Part.assert (p a) fun _ ↦ Part.some ()
suffices ℕ ⊧/![x] ((codeOfPartrec' fun v ↦ Part.map (fun _ ↦ 0) (f (v.get 0)))/[‘0’, #0]) ↔ p x from this
have : Partrec fun v : Vector ℕ 1 ↦ (f (v.get 0)).map fun _ ↦ 0 := by
have : Partrec fun v : Mathlib.Vector ℕ 1 ↦ (f (v.get 0)).map fun _ ↦ 0 := by
refine Partrec.map (Partrec.comp hp (Primrec.to_comp <| Primrec.vector_get.comp .id (.const 0))) (Computable.const 0).to₂
simp [Semiformula.eval_substs, Matrix.comp_vecCons', Matrix.constant_eq_singleton]
apply (codeOfPartrec'_spec (Nat.Partrec'.of_part this) (v := ![x]) (y := 0)).trans (by simp [f])
Expand Down
4 changes: 2 additions & 2 deletions Foundation/IntFO/Translation.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -72,8 +72,8 @@ open Rewriting System System.FiniteContext HilbertProofᵢ

noncomputable
def negDoubleNegation : (φ : SyntacticFormula L) → 𝐌𝐢𝐧¹ ⊢ ∼φᴺ ⭤ (∼φ)ᴺ
| .rel r v => System.tneIff (φ := .rel r v)
| .nrel r v => System.iffId (φ := ∼∼(.rel r v))
| .rel r v => System.tneIff (φ := Semiformulaᵢ.rel r v)
| .nrel r v => System.iffId (φ := ∼∼(Semiformulaᵢ.rel r v))
| ⊤ => System.falsumDN
| ⊥ => System.iffId (φ := ∼⊥)
| φ ⋏ ψ =>
Expand Down
24 changes: 12 additions & 12 deletions Foundation/IntProp/Dialectica/Basic.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,11 +44,11 @@ def Interpret (V : α → Prop) : (φ : Formula α) → Witness φ → Counter
| ∼φ, f, θ => ¬Interpret V φ θ (f θ)
| φ ➝ ψ, ⟨f, g⟩, ⟨θ, π⟩ => Interpret V φ θ (g θ π) → Interpret V ψ (f θ) π

scoped notation "⟦" w " | " c "⟧ ⊩[" V "] " φ:46 => Interpret V φ w c
scoped notation:80 "⟦" w " | " c "⟧⊩[" V "] " φ:46 => Interpret V φ w c

def Valid (φ : Formula α) : Prop := ∃ w, ∀ V c, ⟦w | c⟧ ⊩[V] φ
def Valid (φ : Formula α) : Prop := ∃ w, ∀ V c, ⟦w | c⟧⊩[V] φ

def NotValid (φ : Formula α) : Prop := ∀ w, ∃ V c, ¬⟦w | c⟧ ⊩[V] φ
def NotValid (φ : Formula α) : Prop := ∀ w, ∃ V c, ¬⟦w | c⟧⊩[V] φ

scoped notation "⊩ " φ => Valid φ

Expand All @@ -57,29 +57,29 @@ scoped notation "⊮ " φ => NotValid φ
lemma not_valid_iff_notValid {φ : Formula α} : (¬⊩ φ) ↔ (⊮ φ) := by
simp [Valid, NotValid]

@[simp] lemma interpret_verum {w c V} : ⟦w | c⟧ ⊩[V] (⊤ : Formula α) := trivial
@[simp] lemma interpret_verum {w c V} : ⟦w | c⟧⊩[V] (⊤ : Formula α) := trivial

@[simp] lemma interpret_falsum {w c V} : ¬⟦w | c⟧ ⊩[V] (⊥ : Formula α) := id
@[simp] lemma interpret_falsum {w c V} : ¬⟦w | c⟧⊩[V] (⊥ : Formula α) := id

@[simp] lemma interpret_atom {w c V} {a : α} : (⟦w | c⟧ ⊩[V] .atom a) ↔ V a := Eq.to_iff rfl
@[simp] lemma interpret_atom {w c V} {a : α} : (⟦w | c⟧⊩[V] .atom a) ↔ V a := Eq.to_iff rfl

@[simp] lemma interpret_and_left {φ ψ : Formula α} {V θ π} :
⟦θ | .inl π⟧ ⊩[V] φ ⋏ ψ ↔ ⟦θ.1 | π⟧ ⊩[V] φ := Eq.to_iff rfl
⟦θ | .inl π⟧⊩[V] φ ⋏ ψ ↔ ⟦θ.1 | π⟧⊩[V] φ := Eq.to_iff rfl

@[simp] lemma interpret_and_right {φ ψ : Formula α} {V θ π} :
⟦θ | .inr π⟧ ⊩[V] φ ⋏ ψ ↔ ⟦θ.2 | π⟧ ⊩[V] ψ := Eq.to_iff rfl
⟦θ | .inr π⟧⊩[V] φ ⋏ ψ ↔ ⟦θ.2 | π⟧⊩[V] ψ := Eq.to_iff rfl

@[simp] lemma interpret_or_left {φ ψ : Formula α} {V θ π} :
⟦.inl θ | π⟧ ⊩[V] φ ⋎ ψ ↔ ⟦θ | π.1⟧ ⊩[V] φ := Eq.to_iff rfl
⟦.inl θ | π⟧⊩[V] φ ⋎ ψ ↔ ⟦θ | π.1⟧⊩[V] φ := Eq.to_iff rfl

@[simp] lemma interpret_or_right {φ ψ : Formula α} {V θ π} :
⟦.inr θ | π⟧ ⊩[V] φ ⋎ ψ ↔ ⟦θ | π.2⟧ ⊩[V] ψ := Eq.to_iff rfl
⟦.inr θ | π⟧⊩[V] φ ⋎ ψ ↔ ⟦θ | π.2⟧⊩[V] ψ := Eq.to_iff rfl

@[simp] lemma interpret_not {φ : Formula α} {V θ f} :
⟦f | θ⟧ ⊩[V] ∼φ ↔ ¬⟦θ | f θ⟧ ⊩[V] φ := Eq.to_iff rfl
⟦f | θ⟧⊩[V] ∼φ ↔ ¬⟦θ | f θ⟧⊩[V] φ := Eq.to_iff rfl

@[simp] lemma interpret_imply {φ ψ : Formula α} {V f π} :
⟦f | π⟧ ⊩[V] φ ➝ ψ ↔ (⟦π.1 | f.2 π.1 π.2⟧ ⊩[V] φ → ⟦f.1 π.1 | π.2⟧ ⊩[V] ψ) := Eq.to_iff rfl
⟦f | π⟧⊩[V] φ ➝ ψ ↔ (⟦π.1 | f.2 π.1 π.2⟧⊩[V] φ → ⟦f.1 π.1 | π.2⟧⊩[V] ψ) := Eq.to_iff rfl

protected lemma Valid.refl (φ : Formula α) : ⊩ φ ➝ φ := ⟨⟨id, fun _ π ↦ π⟩, by rintro V ⟨θ, π⟩; simp⟩

Expand Down
Loading

0 comments on commit d5a5b56

Please sign in to comment.