Skip to content

Commit 15f9876

Browse files
author
GBathie
committed
WIP
1 parent 6f26a10 commit 15f9876

2 files changed

Lines changed: 109 additions & 97 deletions

File tree

‎BoltLean/Helpers.lean‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
open Classical
2+
3+
theorem my_contra (a b: Prop): (a → b) ↔ (¬b → ¬a) := by
4+
constructor
5+
. intro himp hnb ha
6+
apply hnb
7+
apply himp
8+
exact ha
9+
. intro himp ha
10+
apply byContradiction
11+
intro hnb
12+
apply absurd
13+
. exact ha
14+
. apply himp
15+
assumption

‎BoltLean/UpperBound.lean‎

Lines changed: 94 additions & 97 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
import BoltLean.Ltl
2+
import BoltLean.Helpers
23

34
namespace Trace
45
def get_exact_var (t: Trace n) (i: Fin t.length) (v: Fin n): Formula n :=
@@ -102,103 +103,99 @@ namespace Trace
102103
. left
103104
exact hl
104105

105-
-- theorem exact_at_pos_eval_iff
106-
-- (t t': Trace n) (i: Fin t.length) (i': Fin t'.length) :
107-
-- (t.exact_at_pos i).eval_aux t' i'
108-
-- ↔ (∀ (v : Fin n), t.predicates[v][i] = t'.predicates[v][i']) := by
109-
-- -- Proof by induction or well-founded recursion on (n - v)
110-
-- constructor
111-
-- . intro h v
112-
-- unfold exact_at_pos at h
113-
-- unfold Formula.eval_aux at h
114-
-- simp at h
115-
-- . sorry
116-
117-
-- theorem not_eval_aux_exact_at_pos_if_diff_pred (t t': Trace n)
118-
-- (i: Fin t.length) (v: Fin n)
119-
-- (hi: i < t'.length) (h: t.predicates[v][i] ≠ t'.predicates[v][i]) :
120-
-- ¬(t.exact_at_pos i v).eval_aux t' ⟨i.val, hi⟩ := by
121-
-- unfold exact_at_pos
122-
-- simp
123-
-- split
124-
-- . next hif =>
125-
-- simp [Formula.eval_aux]
126-
-- intro he
127-
-- simp at h
128-
-- rw [eq_comm] at he
129-
-- exact absurd he h
130-
-- . next hnif => simp [Formula.eval_aux]
131-
-- simp at h
132-
-- rw [eq_comm] at h
133-
-- exact h
134-
135-
-- theorem not_eval_aux_exact_at_pos_if_diff_pred_lt (t t': Trace n)
136-
-- (i: Fin t.length) (v v': Fin n) (hv: v' ≤ v)
137-
-- (hi: i < t'.length) (h: t.predicates[v][i] ≠ t'.predicates[v][i]) :
138-
-- ¬(t.exact_at_pos i v').eval_aux t' ⟨i.val, hi⟩ := by
139-
-- by_cases he: v' = v
140-
-- . rw [he]
141-
-- apply not_eval_aux_exact_at_pos_if_diff_pred <;> assumption
142-
-- . unfold exact_at_pos
143-
-- have hv': v' < n-1 := by omega
144-
-- simp [hv']
145-
-- simp [Formula.eval_aux]
146-
-- intro hp
147-
-- let v'' := v'.val+1
148-
-- have hv'': v'' ≤ v := by omega
149-
-- apply not_eval_aux_exact_at_pos_if_diff_pred_lt t t' i v ⟨v'', by omega⟩ hv'' hi h
150-
151-
-- theorem not_eval_aux_exact_aux_if_diff_pred (t t': Trace n)
152-
-- (i: Fin t.length) (v: Fin n)
153-
-- (hi: i < t'.length) (h: t.predicates[v][i] ≠ t'.predicates[v][i]) :
154-
-- ¬(t.exact_aux i).eval_aux t' ⟨i.val, hi⟩ := by
155-
-- unfold exact_aux
156-
-- split
157-
-- . next hif => simp
158-
-- unfold Formula.eval_aux
159-
-- rw [Classical.not_and_iff_not_or_not]
160-
-- left
161-
-- apply not_eval_aux_exact_at_pos_if_diff_pred_lt
162-
-- all_goals try assumption
163-
-- apply Nat.zero_le
164-
-- . next hnif => simp
165-
-- apply not_eval_aux_exact_at_pos_if_diff_pred_lt
166-
-- all_goals try assumption
167-
-- apply Nat.zero_le
168-
169-
170-
-- theorem not_eval_aux_exact_aux_if_diff_pred_lt (t t': Trace n)
171-
-- (i i': Fin t.length) (hi': i' ≤ i) (v: Fin n)
172-
-- (hi: i < t'.length) (h: t.predicates[v][i] ≠ t'.predicates[v][i]) :
173-
-- ¬(t.exact_aux i').eval_aux t' ⟨i'.val,by omega⟩ := by
174-
-- by_cases he: i = i'
175-
-- . subst he
176-
-- apply not_eval_aux_exact_aux_if_diff_pred <;> assumption
177-
-- . unfold exact_aux
178-
-- simp
179-
-- have h1: i' < t.length - 1 := by omega
180-
-- simp [h1]
181-
-- unfold Formula.eval_aux
182-
-- simp
183-
-- intro h2
184-
-- simp [Formula.eval_aux]
185-
-- intro
186-
-- apply not_eval_aux_exact_aux_if_diff_pred_lt
187-
-- all_goals try assumption
188-
-- rw [Nat.ne_iff_lt_or_gt] at he
189-
-- sorry
190-
191-
-- /-- Soundness: `t.exact` only accepts `t`-/
192-
-- theorem exact_eval_only (t t': Trace n) (h: t ≠ t'): ¬(t.exact).eval t' := by
193-
-- have h1 := diff_exist_diff_var t t' h
194-
-- match h1 with
195-
-- | Or.inl h2 => sorry
196-
-- | Or.inr h2 => match h2 with
197-
-- | ⟨i, v, h', hd⟩ => unfold exact
198-
-- unfold Formula.eval
199-
-- apply not_eval_aux_exact_aux_if_diff_pred t t' i
200-
-- assumption
201-
106+
theorem exact_at_pos_eval_iff
107+
(t t': Trace n) (i: Fin t.length) (i': Fin t'.length) :
108+
(t.exact_at_pos i).eval_aux t' i'
109+
↔ (∀ (v : Fin n), t.predicates[v][i] = t'.predicates[v][i']) := by
110+
-- Proof by induction or well-founded recursion on (n - v)
111+
constructor
112+
. intro h v
113+
unfold exact_at_pos at h
114+
unfold Formula.eval_aux at h
115+
simp at h
116+
. sorry
117+
118+
theorem not_eval_aux_exact_at_pos_if_diff_pred (t t': Trace n)
119+
(i: Fin t.length) (v: Fin n)
120+
(hi: i < t'.length) (h: t.predicates[v][i] ≠ t'.predicates[v][i]) :
121+
¬(t.exact_at_pos i v).eval_aux t' ⟨i.val, hi⟩ := by
122+
unfold exact_at_pos
123+
simp
124+
split
125+
. next hif =>
126+
simp [Formula.eval_aux]
127+
intro he
128+
simp at h
129+
rw [eq_comm] at he
130+
exact absurd he h
131+
. next hnif => simp [Formula.eval_aux]
132+
simp at h
133+
rw [eq_comm] at h
134+
exact h
135+
136+
theorem not_eval_aux_exact_at_pos_if_diff_pred_lt (t t': Trace n)
137+
(i: Fin t.length) (v v': Fin n) (hv: v' ≤ v)
138+
(hi: i < t'.length) (h: t.predicates[v][i] ≠ t'.predicates[v][i]) :
139+
¬(t.exact_at_pos i v').eval_aux t' ⟨i.val, hi⟩ := by
140+
by_cases he: v' = v
141+
. rw [he]
142+
apply not_eval_aux_exact_at_pos_if_diff_pred <;> assumption
143+
. unfold exact_at_pos
144+
have hv': v' < n-1 := by omega
145+
simp [hv']
146+
simp [Formula.eval_aux]
147+
intro hp
148+
let v'' := v'.val+1
149+
have hv'': v'' ≤ v := by omega
150+
apply not_eval_aux_exact_at_pos_if_diff_pred_lt t t' i v ⟨v'', by omega⟩ hv'' hi h
151+
152+
theorem not_eval_aux_exact_aux_if_diff_pred (t t': Trace n)
153+
(i: Fin t.length) (v: Fin n)
154+
(hi: i < t'.length) (h: t.predicates[v][i] ≠ t'.predicates[v][i]) :
155+
¬(t.exact_aux i).eval_aux t' ⟨i.val, hi⟩ := by
156+
unfold exact_aux
157+
split
158+
. next hif => simp
159+
unfold Formula.eval_aux
160+
rw [Classical.not_and_iff_not_or_not]
161+
left
162+
apply not_eval_aux_exact_at_pos_if_diff_pred_lt
163+
all_goals try assumption
164+
apply Nat.zero_le
165+
. next hnif => simp
166+
apply not_eval_aux_exact_at_pos_if_diff_pred_lt
167+
all_goals try assumption
168+
apply Nat.zero_le
169+
170+
171+
theorem not_eval_aux_exact_aux_if_diff_pred_lt (t t': Trace n)
172+
(i i': Fin t.length) (hi': i' ≤ i) (v: Fin n)
173+
(hi: i < t'.length) (h: t.predicates[v][i] ≠ t'.predicates[v][i]) :
174+
¬(t.exact_aux i').eval_aux t' ⟨i'.val,by omega⟩ := by
175+
by_cases he: i = i'
176+
. subst he
177+
apply not_eval_aux_exact_aux_if_diff_pred <;> assumption
178+
. unfold exact_aux
179+
simp
180+
have h1: i' < t.length - 1 := by omega
181+
simp [h1]
182+
unfold Formula.eval_aux
183+
simp
184+
intro h2
185+
simp [Formula.eval_aux]
186+
intro
187+
apply not_eval_aux_exact_aux_if_diff_pred_lt
188+
all_goals try assumption
189+
rw [Nat.ne_iff_lt_or_gt] at he
190+
sorry
191+
192+
open Classical
193+
/-- Soundness: `t.exact` only accepts `t`-/
194+
theorem exact_eval_only (t t': Trace n):
195+
(t.exact).eval t' → t = t' := by
196+
rw [my_contra]
197+
intro hne
198+
sorry
202199
end Trace
203200

204201
-- theorem exact_eval (t: Trace n) :

0 commit comments

Comments
 (0)