Skip to content

Commit e727df9

Browse files
nlohrernlohrer
committed
Add first steps for assignment-invariance of closed formulas.
Has a lot of holes right now, but I really want to have this back up...
1 parent c8ff8ce commit e727df9

File tree

2 files changed

+245
-9
lines changed

2 files changed

+245
-9
lines changed

‎InferenceInLean/Semantics.lean‎

Lines changed: 244 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -77,15 +77,9 @@ def Formula.eval {sig : Signature} {X : Variables} {univ : Universes} [Decidable
7777
| Formula.all x f => ∀ a : univ, Formula.eval I (β.modify x a) f
7878
| Formula.ex x f => ∃ a : univ, Formula.eval I (β.modify x a) f
7979

80-
lemma Formula.eval_of_closed {sig : Signature} {X : Variables} [inst : DecidableEq X]
81-
(I : Interpretation sig univ) (F : Formula sig X) (hclosed : Formula.closed F) :
82-
(∀ (β γ : Assignment X univ), Formula.eval I β F = Formula.eval I γ F) := by
83-
intro β γ
84-
sorry
85-
8680
@[simp]
87-
def Term.eval_without_free {sig : Signature} {X : Variables} [DecidableEq X] (t : Term sig X) :
88-
t.freeVars = {} → ¬∃ (x : X), t = Term.var x := by
81+
lemma Term.eval_without_free_not_term {sig : Signature} {X : Variables} [DecidableEq X]
82+
(t : Term sig X) : t.freeVars = {} → ¬∃ (x : X), t = Term.var x := by
8983
intro a
9084
simp_all only [not_exists]
9185
intro x
@@ -94,7 +88,131 @@ def Term.eval_without_free {sig : Signature} {X : Variables} [DecidableEq X] (t
9488
subst a_1
9589
simp_all only [Term.freeVars.eq_1, Set.singleton_ne_empty]
9690

91+
lemma Set.singleton_of_union_empty {α : Type} {x : α} {A B : Set α}
92+
(h : ¬A = {x}) (hsingleton : A ∪ B = {x}) : A = ∅ := by
93+
have sub : A ⊆ {x} := by
94+
rw [← hsingleton]
95+
exact Set.subset_union_left
96+
have : A = ∅ ∨ A = {x} := by
97+
exact Set.subset_singleton_iff_eq.mp sub
98+
simp_all only [Set.subset_singleton_iff, or_false]
99+
100+
@[simp]
101+
lemma Term.subterms_closed {sig : Signature} {X : Variables} {_I : Interpretation sig univ}
102+
[DecidableEq X] (t : Term sig X) (x : X) :
103+
∀ (f : sig.funs) (args : List (Term sig X)), t = Term.func f args →
104+
t.freeVars = {} →
105+
∀ (arg : Term sig X) (harg : arg ∈ args), arg.freeVars = {} := by
106+
intro f args ht hclosed arg harg
107+
subst ht
108+
induction' args with arg' args' ih generalizing arg
109+
· simp_all only [List.not_mem_nil]
110+
· aesop
111+
112+
@[simp]
113+
lemma Term.one_freeVar_of_subterms {univ : Universes} {sig : Signature} {X : Variables}
114+
(I : Interpretation sig univ) [DecidableEq X] {t : Term sig X} {x : X} :
115+
∀ (f : sig.funs) (args : List (Term sig X)), t = Term.func f args →
116+
t.freeVars = {x} →
117+
∀ (arg : Term sig X) (_harg : arg ∈ args), arg.freeVars = {x} ∨ arg.freeVars = {} := by
118+
intro f args ht honefree arg harg
119+
induction' args with arg' args' ih generalizing arg t
120+
· simp_all only [Term.freeVars.eq_2, Term.func.injEq, or_self, List.not_mem_nil]
121+
· simp_all only [Term.freeVars.eq_3, Term.func.injEq, List.cons_ne_self, and_false,
122+
IsEmpty.forall_iff, implies_true, List.mem_cons]
123+
by_cases h : Term.freeVars sig X arg = {x}
124+
· left
125+
exact h
126+
· rcases harg with h₁ | h₂
127+
· subst h₁
128+
subst ht
129+
simp_all only [false_or]
130+
clear ih
131+
generalize Term.freeVars sig X arg = A, Term.freeVars sig X (Term.func f args') = B at *
132+
exact Set.singleton_of_union_empty h honefree
133+
· subst ht
134+
simp_all only [false_or]
135+
specialize @ih (Term.func f args') rfl
136+
by_cases h' : Term.freeVars sig X (Term.func f args') = {x}
137+
· specialize ih h' arg h₂
138+
simp_all only [Set.union_singleton, false_or]
139+
· simp_all only [IsEmpty.forall_iff]
140+
generalize hA : Term.freeVars sig X (Term.func f args') = A,
141+
hB : Term.freeVars sig X arg' = B at *
142+
have hempty : A = {} := by
143+
rw [Set.union_comm] at honefree
144+
exact Set.singleton_of_union_empty h' honefree
145+
clear honefree
146+
induction' args' with arg' args ih
147+
· simp_all only [List.not_mem_nil]
148+
· aesop
149+
150+
@[simp]
151+
lemma Assignment.eval_closed_term {sig : Signature} {X : Variables} {I : Interpretation sig univ}
152+
[DecidableEq X] (t : Term sig X)
153+
(x : X) : t.freeVars = {} → ∀ (β γ : Assignment X univ) (a : univ),
154+
Term.eval I β t = Term.eval I γ t := by
155+
intro hclosed β γ a
156+
induction' t using Term.induction with y args ih f generalizing β γ a
157+
· simp_all only [Term.freeVars.eq_1, Set.singleton_ne_empty]
158+
· simp_all only [Assignment, Term.eval, List.map_subtype, List.unattach_attach]
159+
have hargsareequal : List.map (Term.eval I β) args =
160+
List.map (Term.eval I γ) args := by
161+
simp_all only [List.map_inj_left]
162+
intro arg harg
163+
have s := @Term.subterms_closed univ sig X I _ (Term.func f args) x f args rfl hclosed arg harg
164+
specialize ih arg harg s β γ a
165+
rw [ih]
166+
rw [← hargsareequal]
167+
168+
#check Term.subterms_closed
97169

170+
@[simp]
171+
lemma Assignment.eval_term_with_one_free {univ : Universes} {sig : Signature} {X : Variables}
172+
{I : Interpretation sig univ} [DecidableEq X] {t : Term sig X}
173+
{x : X} : t.freeVars = {x} → ∀ (β γ : Assignment X univ) (a : univ),
174+
Term.eval I (β.modify x a) t = Term.eval I (γ.modify x a) t := by
175+
intro honefree β γ a
176+
induction' t using Term.induction with y args ih f
177+
· simp_all only [Term.freeVars.eq_1, Set.singleton_eq_singleton_iff, Term.eval, modify,
178+
↓reduceIte]
179+
· simp_all only [Term.eval, List.map_subtype, List.unattach_attach]
180+
have hargsareequal :
181+
List.map (Term.eval I (β.modify x a)) args = List.map (Term.eval I (γ.modify x a)) args := by
182+
simp_all only [List.map_inj_left]
183+
intro arg harg
184+
have honeornone := Term.one_freeVar_of_subterms I f args rfl honefree arg harg
185+
rcases honeornone with hone | hnone
186+
· aesop
187+
· apply Assignment.eval_closed_term
188+
· exact x
189+
· simp_all only
190+
· exact a
191+
rw [hargsareequal]
192+
193+
/- @[simp]
194+
def Term.eval_without_free {sig : Signature} {X : Variables} [DecidableEq X] (t : Term sig X) :
195+
t.freeVars = {} → ∀ (f : sig.funs) (args : List (Term sig X)),
196+
t = Term.func f args → args = [] := by
197+
intro hclosed f args heq
198+
by_contra harg
199+
induction' t using Term.induction with x args ih f generalizing args
200+
· sorry
201+
·
202+
simp_all only [imp_false, not_not, Term.func.injEq]
203+
obtain ⟨left, right⟩ := heq
204+
subst left right
205+
apply harg
206+
have hex : ∃ (t : Term sig X), t ∈ args := List.exists_mem_of_ne_nil args harg
207+
rcases hex with ⟨arg, harg⟩
208+
specialize ih (Term.func f args)
209+
have h : ∀ term ∈ args,
210+
Term.freeVars sig X term = ∅ → ∀ (args : List (Term sig X)), term = Term.func f args := sorry
211+
specialize ih h -/
212+
213+
#check Formula.freeVars
214+
#check Set.mem_diff_singleton
215+
#check Term.freeVars
98216
-- β[x1 ↦ a1, ..., xn ↦ an]
99217
@[simp]
100218
def Assignment.bigModify {X : Variables} {univ : Universes} [DecidableEq X]
@@ -104,6 +222,29 @@ def Assignment.bigModify {X : Variables} {univ : Universes} [DecidableEq X]
104222
| x :: xs, a :: as => Assignment.bigModify (β.modify x a) xs as
105223
| _, _ => β
106224

225+
def Assignment.bigModify_modify {X : Variables} {univ : Universes} [DecidableEq X]
226+
(β : Assignment X univ) (xs : List X) (as : List univ) (y : X) (b : univ) (hxuniq : xs.Nodup)
227+
(hxnotinxs : y ∉ xs) (n : ℕ) (hn : n = xs.length) (hlen : xs.length = as.length) :
228+
(β.bigModify xs as).modify y b = (β.modify y b).bigModify xs as := by
229+
induction' n with n ih generalizing xs as β
230+
· have hxsempty : xs = [] := by exact List.length_eq_zero.mp (id (Eq.symm hn))
231+
have hasempty : as = [] := by subst hxsempty; exact List.length_eq_zero.mp (id (Eq.symm hlen))
232+
subst hxsempty hasempty
233+
simp_all only [List.nodup_nil, List.not_mem_nil, not_false_eq_true, List.length_nil, Assignment,
234+
bigModify]
235+
· match xs, as with
236+
| x :: xs, a :: as =>
237+
rw [bigModify, bigModify]
238+
specialize ih (β.modify x a) xs as (List.Nodup.of_cons hxuniq)
239+
(List.not_mem_of_not_mem_cons hxnotinxs)
240+
(by simp_all only [Assignment, List.nodup_cons, List.mem_cons, not_or, List.length_cons,
241+
Nat.add_right_cancel_iff])
242+
(by exact Nat.succ_inj'.mp hlen)
243+
rw [ih, modify_comm x y a b (Ne.symm (List.ne_of_not_mem_cons hxnotinxs))]
244+
| [], [] =>
245+
simp_all only [List.nodup_nil, List.not_mem_nil, not_false_eq_true, List.length_nil,
246+
bigModify, implies_true, Nat.add_one_ne_zero]
247+
107248
-- β[] = β
108249
@[simp]
109250
lemma Assignment.bigModify_empty {X : Variables} {univ : Universes} [DecidableEq X]
@@ -320,3 +461,98 @@ lemma Assignment.modFn_eq_id {X : Variables} {univ : Universes} [DecidableEq X]
320461
· have hasnone : as[i]? = none := getElem?_neg as i hin
321462
have hxsnone : xs[i]? = none := by simp_all only [not_lt, getElem?_eq_none]
322463
rw [hasnone, hxsnone, Option.map]
464+
465+
466+
lemma Formula.eval_of_many_free {sig : Signature} {X : Variables} [inst : DecidableEq X]
467+
(I : Interpretation sig univ) (F : Formula sig X) (xs : List X) (as : List univ)
468+
(hxuniq : xs.Nodup) (hlen : xs.length = as.length) (hfree : F.freeVars = xs.toFinset) :
469+
(∀ (β γ : Assignment X univ),
470+
Formula.eval I (β.bigModify xs as) F = Formula.eval I (γ.bigModify xs as) F) := by
471+
intro β γ
472+
induction' F with _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ x F ih y f ih generalizing β γ xs as
473+
· simp_all only [Formula.freeVars, eval]
474+
· simp_all only [Formula.freeVars, eval]
475+
· sorry
476+
· sorry
477+
· sorry
478+
· sorry
479+
· sorry
480+
· sorry
481+
· simp_all only [Assignment, eq_iff_iff, Formula.freeVars, eval]
482+
apply Iff.intro
483+
· intro heval a
484+
specialize heval a
485+
by_cases hxinxs : x ∈ xs
486+
· by_contra hcontra
487+
clear heval hcontra ih
488+
have hxinxs₂ : x ∈ {a | a ∈ xs} := by simp_all only [List.coe_toFinset, Set.mem_setOf_eq]
489+
clear hxinxs
490+
rw [List.coe_toFinset] at hfree
491+
generalize {a | a ∈ xs} = A, F.freeVars = B at *
492+
subst hfree
493+
simp_all only [Set.mem_diff, Set.mem_singleton_iff, not_true_eq_false, and_false]
494+
· by_cases hfin : F.freeVars = ↑xs.toFinset ∪ {x}
495+
· have hfreexxs : F.freeVars = ↑(x :: xs).toFinset := by
496+
simp_all only [List.coe_toFinset, Set.union_singleton, Set.mem_singleton_iff,
497+
Set.insert_diff_of_mem, Set.mem_setOf_eq, not_false_eq_true,
498+
Set.diff_singleton_eq_self, List.toFinset_cons, Finset.coe_insert]
499+
specialize ih (x :: xs) (a :: as) (List.Nodup.cons hxinxs hxuniq)
500+
(Nat.succ_inj'.mpr hlen) hfreexxs β γ
501+
rw [Assignment.bigModify, Assignment.bigModify] at ih
502+
rw [Assignment.bigModify_modify γ xs as x a hxuniq hxinxs xs.length rfl hlen]
503+
apply ih.mp
504+
rw [← Assignment.bigModify_modify β xs as x a hxuniq hxinxs xs.length rfl hlen]
505+
exact heval
506+
· have hfreexs : F.freeVars = ↑xs.toFinset := by
507+
clear ih heval hlen hxuniq
508+
rw [List.coe_toFinset] at *
509+
have hxnotinxs : x ∉ {a | a ∈ xs} := by
510+
simp_all only [Set.union_singleton, Set.mem_setOf_eq, not_false_eq_true]
511+
clear hxinxs
512+
generalize {a | a ∈ xs} = A, F.freeVars = B at *
513+
aesop
514+
specialize ih xs as hxuniq hlen hfreexs (β.modify x a) (γ.modify x a)
515+
rw [Assignment.bigModify_modify γ xs as x a hxuniq hxinxs xs.length rfl hlen]
516+
apply ih.mp
517+
rw [← Assignment.bigModify_modify β xs as x a hxuniq hxinxs xs.length rfl hlen]
518+
exact heval
519+
· sorry -- completely analogous
520+
· sorry
521+
522+
lemma Formula.eval_of_closed {sig : Signature} {X : Variables} [inst : DecidableEq X]
523+
(I : Interpretation sig univ) (F : Formula sig X) (hclosed : Formula.closed F) :
524+
(∀ (β γ : Assignment X univ), Formula.eval I β F = Formula.eval I γ F) := by
525+
intro β γ
526+
induction' F with _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ x F ih x f ih generalizing β γ
527+
· simp_all only [Formula.closed, Formula.freeVars, eval]
528+
· simp_all only [Formula.closed, Formula.freeVars, eval]
529+
· sorry
530+
· sorry
531+
· sorry
532+
· sorry
533+
· sorry
534+
· sorry
535+
·
536+
simp_all only [Formula.closed, eq_iff_iff, Formula.freeVars, eval]
537+
by_cases h : F.freeVars = ∅
538+
· simp_all only [Assignment, forall_const, Set.mem_empty_iff_false, not_false_eq_true, Set.diff_singleton_eq_self]
539+
apply Iff.intro
540+
· intro hmod a
541+
specialize ih (β.modify x a) (γ.modify x a)
542+
simp_all only [true_iff]
543+
· intro hmod a
544+
specialize ih (β.modify x a) (γ.modify x a)
545+
simp_all only [iff_true]
546+
apply Iff.intro
547+
· intro hmod a
548+
simp_all only [Assignment, IsEmpty.forall_iff]
549+
have honefree : F.freeVars = {x} := by
550+
generalize F.freeVars = A at *
551+
ext y
552+
sorry
553+
clear hclosed h
554+
sorry
555+
· intro hmod a
556+
simp_all only [Assignment, IsEmpty.forall_iff]
557+
sorry
558+
· sorry

‎InferenceInLean/Syntax.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -102,7 +102,7 @@ inductive Formula where
102102
| ex (x : X) (f : Formula)
103103

104104
@[simp]
105-
def Formula.freeVars {sig : Signature} {X : Variables} : @Formula sig X -> Set X
105+
def Formula.freeVars {sig : Signature} {X : Variables} : Formula sig X -> Set X
106106
| Formula.falsum => ∅
107107
| Formula.verum => ∅
108108
| Formula.atom a => Atom.freeVars a

0 commit comments

Comments
 (0)