Skip to content

Commit 5239adf

Browse files
nlohrernlohrer
committed
Finish proof for Clause.closedClause_closed
▪
1 parent 1da1ab7 commit 5239adf

File tree

2 files changed

+228
-2
lines changed

2 files changed

+228
-2
lines changed

‎InferenceInLean/Semantics.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -170,7 +170,8 @@ lemma Assignment.eval_term_with_one_free {univ : Universes} {sig : Signature} {X
170170
↓reduceIte]
171171
· simp_all only [Term.eval, List.map_subtype, List.unattach_attach]
172172
have hargsareequal :
173-
List.map (Term.eval I (β.modify x a)) args = List.map (Term.eval I (γ.modify x a)) args := by
173+
List.map (Term.eval I (β.modify x a)) args =
174+
List.map (Term.eval I (γ.modify x a)) args := by
174175
simp_all only [List.map_inj_left]
175176
intro arg harg
176177
have honeornone := Term.one_freeVar_of_subterms I f args rfl honefree arg harg

‎InferenceInLean/Syntax.lean‎

Lines changed: 226 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -144,6 +144,47 @@ def Formula.bigForall [DecidableEq X]
144144
| [] => F
145145
| x :: xs => .all x (F.bigForall xs)
146146

147+
@[simp]
148+
lemma Formula.bigForall_freeVars_subset [DecidableEq X] (xs : List X) (F : Formula sig X) :
149+
(F.bigForall sig X xs).freeVars ⊆ F.freeVars := by
150+
induction' xs with x xs ih
151+
· simp_all only [bigForall, subset_refl]
152+
· simp_all only [bigForall, freeVars, Set.diff_singleton_subset_iff]
153+
intro x' hx'
154+
simp_all only [Set.mem_insert_iff]
155+
apply Or.inr
156+
apply ih
157+
simp_all only
158+
159+
lemma Formula.bigForall_all [DecidableEq X] (xs : List X) (F : Formula sig X) (x : X) :
160+
(bigForall sig X xs (all x F)).freeVars = (all x (bigForall sig X xs F)).freeVars := by
161+
simp_all only [freeVars]
162+
induction' xs with y xs ih
163+
· simp_all only [List.not_mem_nil, or_false, Set.setOf_eq_eq_singleton,
164+
Set.subset_singleton_iff, bigForall, freeVars]
165+
· simp_all only [List.mem_cons, bigForall, freeVars]
166+
ext x_1 : 1
167+
simp_all only [Set.mem_diff, Set.mem_singleton_iff]
168+
apply Iff.intro
169+
· intro a
170+
simp_all only [not_false_eq_true, and_self]
171+
· intro a
172+
simp_all only [not_false_eq_true, and_self]
173+
174+
@[simp]
175+
lemma Formula.bigForall_subset_freeVars [DecidableEq X] (xs : List X) (F : Formula sig X) :
176+
F.freeVars ⊆ xs.toFinset → (F.bigForall sig X xs).closed := by
177+
intro hmem
178+
simp_all only [List.coe_toFinset, closed]
179+
induction' xs with x xs ih generalizing F
180+
· simp_all only [List.not_mem_nil, Set.setOf_false, Set.subset_empty_iff, bigForall]
181+
· rw [bigForall, freeVars]
182+
simp_all only [List.mem_cons, bigForall, freeVars]
183+
specialize ih (.all x F)
184+
(by simp_all only [freeVars, Set.diff_singleton_subset_iff]; exact hmem)
185+
have hsymm := bigForall_all sig X xs F x
186+
simp_all only [freeVars]
187+
147188
@[simp]
148189
def Clause.toFormula : Clause sig X -> Formula sig X
149190
| [] => Formula.falsum
@@ -184,6 +225,42 @@ lemma Term.freeVars_sub_freeVarsList [DecidableEq X] (t : Term sig X) :
184225
intro x hxinfree
185226
aesop
186227

228+
@[simp]
229+
lemma Term.freeVarsList_sub_freeVars [DecidableEq X] (t : Term sig X) :
230+
↑(t.freeVarsList).toFinset ⊆ t.freeVars := by
231+
induction' t using Term.induction with x args ih f
232+
· simp_all only [freeVarsList, List.toFinset_cons, List.toFinset_nil, insert_emptyc_eq,
233+
Finset.coe_singleton, freeVars, subset_refl]
234+
· induction' args with arg args ih' generalizing f
235+
· simp_all only [List.not_mem_nil, List.coe_toFinset, IsEmpty.forall_iff, implies_true,
236+
freeVarsList, List.toFinset_nil, Finset.coe_empty, freeVars, subset_refl]
237+
· simp_all only [List.coe_toFinset, List.mem_cons, forall_eq_or_imp, freeVarsList,
238+
List.append_eq, List.mem_dedup,
239+
List.mem_append, freeVars, implies_true, forall_const]
240+
obtain ⟨ihleft, ihright⟩ := ih
241+
intro x hx
242+
simp_all only [Set.mem_setOf_eq, Set.mem_union]
243+
cases hx with
244+
| inl h =>
245+
apply Or.inl
246+
apply ihleft
247+
simp_all only [Set.mem_setOf_eq]
248+
| inr h_1 =>
249+
right
250+
clear ihleft
251+
induction' args with arg' args' ih'
252+
· simp_all only [List.not_mem_nil, IsEmpty.forall_iff, implies_true, freeVarsList]
253+
· simp_all only [List.mem_cons, or_true, implies_true, forall_const, forall_eq_or_imp,
254+
freeVarsList, List.append_eq, List.mem_dedup, List.mem_append, freeVars, Set.mem_union]
255+
obtain ⟨left, right⟩ := ihright
256+
cases h_1 with
257+
| inl h =>
258+
apply Or.inl
259+
apply left
260+
simp_all only [Set.mem_setOf_eq]
261+
| inr h_2 => simp_all only [forall_const, or_true]
262+
263+
@[simp]
187264
def Atom.freeVarsList [DecidableEq X] : Atom sig X -> List X
188265
| .pred _ [] => []
189266
| .pred P (t :: ts) => List.dedup ((t.freeVarsList).append (Atom.pred P ts).freeVarsList)
@@ -211,11 +288,110 @@ def Atom.freeVars_sub_freeVarsList [DecidableEq X] (a : Atom sig X) :
211288
apply ih
212289
exact hxinfree
213290

291+
def Atom.freeVarsList_sub_freeVars[DecidableEq X] (a : Atom sig X) :
292+
↑(a.freeVarsList).toFinset ⊆ a.freeVars := by
293+
induction' a with p args
294+
intro x hmem
295+
simp_all only [List.coe_toFinset, Set.mem_setOf_eq]
296+
induction' args with arg args ih
297+
· simp_all only [freeVarsList, List.not_mem_nil]
298+
· simp_all only [freeVarsList, List.append_eq, List.mem_dedup, List.mem_append, freeVars,
299+
Set.mem_union]
300+
cases hmem with
301+
| inl h =>
302+
left
303+
have l := Term.freeVarsList_sub_freeVars sig X arg
304+
simp_all only [List.coe_toFinset]
305+
apply l
306+
simp_all only [Set.mem_setOf_eq]
307+
| inr h_1 => simp_all only [forall_const, or_true]
308+
309+
@[simp]
214310
def Clause.freeVarsList [DecidableEq X] : Clause sig X -> List X
215311
| [] => []
216312
| (.pos l) :: ls => List.dedup (l.freeVarsList ++ freeVarsList ls)
217313
| (.neg l) :: ls => List.dedup (l.freeVarsList ++ freeVarsList ls)
218314

315+
def Clause.freeVars_sub_freeVarsList [DecidableEq X] (C : Clause sig X) :
316+
(C.toFormula).freeVars ⊆ ↑(C.freeVarsList).toFinset := by
317+
induction' C with lit lits ih
318+
· simp_all only [freeVarsList, List.toFinset_nil, Finset.coe_empty, toFormula, Formula.freeVars,
319+
subset_refl]
320+
· simp_all only [List.coe_toFinset]
321+
match lit with
322+
| .pos a =>
323+
simp_all only [freeVarsList, List.mem_dedup, List.mem_append, toFormula, Formula.freeVars]
324+
intro x
325+
intro a_1
326+
simp_all only [Set.mem_setOf_eq, Set.mem_union]
327+
cases a_1 with
328+
| inl h =>
329+
left
330+
have hfree := Atom.freeVars_sub_freeVarsList sig X a
331+
simp_all only [List.coe_toFinset]
332+
apply hfree
333+
simp_all only [Set.mem_setOf_eq]
334+
| inr h_1 =>
335+
apply Or.inr
336+
apply ih
337+
simp_all only [Set.mem_setOf_eq]
338+
| .neg a =>
339+
simp_all only [freeVarsList, List.mem_dedup, List.mem_append, toFormula, Formula.freeVars]
340+
intro x
341+
intro a_1
342+
simp_all only [Set.mem_setOf_eq, Set.mem_union]
343+
cases a_1 with
344+
| inl h =>
345+
left
346+
have hfree := Atom.freeVars_sub_freeVarsList sig X a
347+
simp_all only [List.coe_toFinset]
348+
apply hfree
349+
simp_all only [Set.mem_setOf_eq]
350+
| inr h_1 =>
351+
apply Or.inr
352+
apply ih
353+
simp_all only [Set.mem_setOf_eq]
354+
355+
def Clause.freeVarsList_sub_freeVars [DecidableEq X] (C : Clause sig X) :
356+
↑(C.freeVarsList).toFinset ⊆ (C.toFormula).freeVars := by
357+
induction' C with lit lits ih
358+
· simp_all only [freeVarsList, List.toFinset_nil, Finset.coe_empty, toFormula, Formula.freeVars,
359+
subset_refl]
360+
· simp_all only [List.coe_toFinset]
361+
match lit with
362+
| .pos a =>
363+
simp_all only [freeVarsList, List.mem_dedup, List.mem_append, toFormula, Formula.freeVars]
364+
intro x
365+
intro a_1
366+
simp_all only [Set.mem_setOf_eq, Set.mem_union]
367+
cases a_1 with
368+
| inl h =>
369+
left
370+
have hfree := Atom.freeVarsList_sub_freeVars sig X a
371+
simp_all only [List.coe_toFinset]
372+
apply hfree
373+
simp_all only [Set.mem_setOf_eq]
374+
| inr h_1 =>
375+
apply Or.inr
376+
apply ih
377+
simp_all only [Set.mem_setOf_eq]
378+
| .neg a =>
379+
simp_all only [freeVarsList, List.mem_dedup, List.mem_append, toFormula, Formula.freeVars]
380+
intro x
381+
intro a_1
382+
simp_all only [Set.mem_setOf_eq, Set.mem_union]
383+
cases a_1 with
384+
| inl h =>
385+
left
386+
have hfree := Atom.freeVarsList_sub_freeVars sig X a
387+
simp_all only [List.coe_toFinset]
388+
apply hfree
389+
simp_all only [Set.mem_setOf_eq]
390+
| inr h_1 =>
391+
apply Or.inr
392+
apply ih
393+
simp_all only [Set.mem_setOf_eq]
394+
219395
@[simp]
220396
lemma nodup_clauseFreeVarsList [DecidableEq X] (C : Clause sig X) :
221397
List.Nodup (C.freeVarsList) := by
@@ -233,7 +409,56 @@ lemma Clause.closedEmpty_closed [DecidableEq X] :
233409
lemma Clause.consClosed [DecidableEq X] (L : Literal sig X) (C : Clause sig X) :
234410
(Clause.toClosedFormula sig X C).closed → (Clause.toClosedFormula sig X (L :: C)).closed := by
235411
intro h
236-
sorry
412+
simp_all only [toClosedFormula]
413+
match L with
414+
| .pos a =>
415+
simp_all only [freeVarsList, List.append_nil, toFormula]
416+
have f := Formula.bigForall_subset_freeVars sig X
417+
(Atom.freeVarsList sig X a ++ freeVarsList sig X C).dedup
418+
((Formula.atom a).or (toFormula sig X C))
419+
apply f
420+
simp_all only [Formula.closed, List.coe_toFinset, List.mem_dedup, List.mem_append,
421+
Formula.freeVars]
422+
intro x
423+
intro a_1
424+
simp_all only [Set.mem_setOf_eq, Set.mem_union]
425+
cases a_1 with
426+
| inl h_1 =>
427+
left
428+
have s := Atom.freeVars_sub_freeVarsList sig X a
429+
simp_all only [List.coe_toFinset]
430+
apply s
431+
simp_all only [Set.mem_setOf_eq]
432+
| inr h_2 =>
433+
have s := Clause.freeVars_sub_freeVarsList sig X C
434+
simp_all only [List.coe_toFinset]
435+
apply Or.inr
436+
apply s
437+
simp_all only [Set.mem_setOf_eq]
438+
| .neg a =>
439+
simp_all only [freeVarsList, List.append_nil, toFormula]
440+
have f := Formula.bigForall_subset_freeVars sig X
441+
(Atom.freeVarsList sig X a ++ freeVarsList sig X C).dedup
442+
((Formula.atom a).neg.or (toFormula sig X C))
443+
simp_all only [Formula.closed, List.coe_toFinset, List.mem_dedup, List.mem_append,
444+
Formula.freeVars]
445+
apply f
446+
intro x
447+
intro a_1
448+
simp_all only [Set.mem_setOf_eq, Set.mem_union]
449+
cases a_1 with
450+
| inl h_1 =>
451+
left
452+
have s := Atom.freeVars_sub_freeVarsList sig X a
453+
simp_all only [List.coe_toFinset]
454+
apply s
455+
simp_all only [Set.mem_setOf_eq]
456+
| inr h_2 =>
457+
have s := Clause.freeVars_sub_freeVarsList sig X C
458+
simp_all only [List.coe_toFinset]
459+
apply Or.inr
460+
apply s
461+
simp_all only [Set.mem_setOf_eq]
237462

238463
theorem Clause.closedClause_closed [DecidableEq X] (C : Clause sig X) :
239464
Formula.closed C.toClosedFormula := by

0 commit comments

Comments
 (0)