Skip to content

Commit b550615

Browse files
SamuelLessSamuelLess
committed
Rename files for better structure
1 parent b38a74b commit b550615

File tree

10 files changed

+22
-73
lines changed

10 files changed

+22
-73
lines changed

‎InferenceInLean.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
11
-- This module serves as the root of the `InferenceInLean` library.
22
-- Import modules here that should be built as part of the library.
3-
import «InferenceInLean».Resolution
3+
import «InferenceInLean».F_Resolution

InferenceInLean/Syntax.lean renamed to InferenceInLean/A_Syntax.lean

File renamed without changes.

InferenceInLean/Semantics.lean renamed to InferenceInLean/B_Semantics.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
import InferenceInLean.Syntax
1+
import InferenceInLean.A_Syntax
22

33
set_option autoImplicit false
44
--set_option diagnostics true

InferenceInLean/Models.lean renamed to InferenceInLean/C_Models.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
import InferenceInLean.Syntax
2-
import InferenceInLean.Semantics
1+
import InferenceInLean.A_Syntax
2+
import InferenceInLean.B_Semantics
33

44
set_option autoImplicit false
55
--set_option diagnostics true

InferenceInLean/Unification.lean renamed to InferenceInLean/D_Unification.lean

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
import InferenceInLean.Syntax
2-
import InferenceInLean.Semantics
3-
import InferenceInLean.Models
1+
import InferenceInLean.A_Syntax
2+
import InferenceInLean.B_Semantics
3+
import InferenceInLean.C_Models
44

55
set_option autoImplicit false
66
--set_option diagnostics true

InferenceInLean/Inference.lean renamed to InferenceInLean/E_Inference.lean

Lines changed: 7 additions & 58 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
1-
import InferenceInLean.Syntax
2-
import InferenceInLean.Semantics
3-
import InferenceInLean.Models
4-
import InferenceInLean.Unification
1+
import InferenceInLean.A_Syntax
2+
import InferenceInLean.B_Semantics
3+
import InferenceInLean.C_Models
4+
import InferenceInLean.D_Unification
55

66
set_option autoImplicit false
77
--set_option diagnostics true
@@ -25,7 +25,7 @@ structure Inference where
2525
conclusion : Clause sig X
2626
condition: Prop
2727

28-
def InferenceSystem := List (Inference sig X)
28+
abbrev InferenceSystem := List (Inference sig X)
2929

3030
instance : Membership (Inference sig X) (InferenceSystem sig X) :=
3131
List.instMembership
@@ -67,57 +67,6 @@ the lecture notes. This means that we can show the soundness of an inference sys
6767
showing that all of its inferences are sound. -/
6868
theorem generalSoundness_of_soundness [inst : DecidableEq X]
6969
(Γ : InferenceSystem sig X) : @Soundness _ _ univ _ Γ → @GeneralSoundness _ _ univ _ Γ := by
70+
/- The proof that was here before only worked due to a wrong definition of ClauseSetEntails.
71+
However, the proof was still correct at least for variables being the Empty type. -/
7072
sorry
71-
/-
72-
intro hsound N F hproof A β hgstrue
73-
rcases hproof with ⟨proof, ⟨hassumptions, hconclusion⟩⟩
74-
have hproofsequencetrue : ∀ F ∈ proof.clauses, EntailsInterpret A β F := by
75-
have hindicestrue : ∀ i (hindex : i < proof.clauses.length),
76-
EntailsInterpret A β proof.clauses[i] := by
77-
intro i hlen
78-
induction' i using Nat.case_strong_induction_on with i ih
79-
· have hvalid := proof.is_valid 0 hlen
80-
aesop
81-
· have hvalid := proof.is_valid (i + 1) hlen
82-
rcases hvalid with hassump | hconseq
83-
· simp_all only [Soundness, SetEntails, Assignment, EntailsInterpret]
84-
· rcases hconseq with ⟨inference, ⟨hin, ⟨hlast, hcond, hprev⟩⟩⟩
85-
rw [hlast]
86-
have hinfsound := hsound inference hin
87-
apply hinfsound
88-
· exact hcond
89-
· intro inf_form hprem
90-
have hinftrue := hprev inf_form hprem
91-
rcases hinftrue with ⟨j, ⟨hjindex, heq⟩⟩
92-
have hjtrue := ih j (Nat.le_of_lt_succ hjindex) (Nat.lt_trans hjindex hlen)
93-
rw [heq]
94-
exact hjtrue
95-
intro F hF
96-
have hfindex : ∃ (i : ℕ) (hindex : i < proof.clauses.length), proof.clauses[i] = F :=
97-
List.mem_iff_getElem.mp hF
98-
aesop
99-
have hlen : proof.clauses.length - 1 < proof.clauses.length := by
100-
have hlennonzero : proof.clauses.length ≠ 0 := by
101-
have hnonempty := proof.clauses_not_empty
102-
simp_all only [List.empty_eq, ne_eq, List.length_eq_zero, not_false_eq_true]
103-
exact Nat.sub_one_lt hlennonzero
104-
have hfconclusion := proof.is_valid (proof.clauses.length - 1) hlen
105-
have hfislast : proof.clauses[proof.clauses.length - 1] = F := by
106-
rw [proof.last_clause_conclusion, hconclusion]
107-
rw [hfislast] at hfconclusion
108-
rcases hfconclusion with hl | hr
109-
· simp_all only [Soundness, SetEntails, Assignment, EntailsInterpret]
110-
· subst hassumptions hconclusion
111-
obtain ⟨inference, h⟩ := hr
112-
obtain ⟨hinf, right⟩ := h
113-
obtain ⟨hconcs, hcond, hforms⟩ := right
114-
have h := hsound inference hinf
115-
rw [hconcs]
116-
apply h
117-
· exact hcond
118-
· intro G hgprem
119-
have hinf := hforms G hgprem
120-
rcases hinf with ⟨j, hjnotconc, hginforms⟩
121-
simp_all only [Soundness, SetEntails, Assignment, EntailsInterpret,
122-
implies_true, List.getElem_mem]
123-
-/

‎InferenceInLean/Exercises/Exercise4.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
import InferenceInLean.Resolution
1+
import InferenceInLean.F_Resolution
22
import Mathlib.Data.Finset.Defs
33

44
set_option autoImplicit false

‎InferenceInLean/Exercises/Exercise5.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
import InferenceInLean.Resolution
1+
import InferenceInLean.F_Resolution
22
import Mathlib.Data.Finset.Defs
33
import Mathlib.Data.Set.Card
44
import Mathlib.SetTheory.Cardinal.Finite

InferenceInLean/Resolution.lean renamed to InferenceInLean/F_Resolution.lean

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
1-
import InferenceInLean.Syntax
2-
import InferenceInLean.Semantics
3-
import InferenceInLean.Models
4-
import InferenceInLean.Unification
5-
import InferenceInLean.Inference
1+
import InferenceInLean.A_Syntax
2+
import InferenceInLean.B_Semantics
3+
import InferenceInLean.C_Models
4+
import InferenceInLean.D_Unification
5+
import InferenceInLean.E_Inference
66

77
set_option autoImplicit false
88
--set_option diagnostics true

InferenceInLean/Examples.lean renamed to InferenceInLean/G_Examples.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
import InferenceInLean.Resolution
1+
import InferenceInLean.F_Resolution
22
import Mathlib.Data.Finset.Defs
33

44
set_option autoImplicit false

0 commit comments

Comments
 (0)