max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test(tests/playground/partial_eq_lemma): partial equation lemmas

Browse source 
@kha I added this example as a template for what the equation compiler
will have to do. The plan is:
- We can use `partial` to define any function if the result type is
inhabited.
- If the result type is of the form `Partial a`, the equation compiler
generates lemmas of the form:

```
theorem fooEq args : terminates (foo args) → foo args = lhs
```
The new test contains an example.
This commit is contained in:
Leonardo de Moura 2019-03-26 18:00:32 -07:00
parent 9ddc778ac3
commit 829a50ccf7
1 changed files with 78 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

78
tests/playground/partial_eq_lemma.lean Normal file
View file

@ -0,0 +1,78 @@
universes u
inductive Partial (α : Type u)
| val (a : α) : Partial
| bot {} : Partial
def terminates {α : Type u} (p : Partial α) : Prop := p ≠ Partial.bot
def fooAux (s : String) (c : Char) : Nat → String.Pos → Partial String.Pos
| 0 i := Partial.bot
| (Nat.succ k) i :=
if s.atEnd i then Partial.val i
else if s.get i == c then Partial.val i
else fooAux k (s.next i)
theorem fooAuxEqSucc (s : String) (c : Char) : ∀ (k : Nat) (i : String.Pos), terminates (fooAux s c k i) → fooAux s c k.succ i = fooAux s c k i
| 0 i ht := absurd rfl ht
| (Nat.succ k) i ht :=
show (fooAux s c k.succ.succ i = fooAux s c k.succ i), from
Decidable.byCases
(λ h : s.atEnd i,
have h₁ : fooAux s c (k.succ.succ) i = Partial.val i, from ifPos h,
have h₂ : fooAux s c k.succ i = Partial.val i, from ifPos h,
Eq.trans h₁ h₂.symm)
(λ h : ¬ s.atEnd i,
Decidable.byCases
(λ h' : s.get i == c,
have h₁ : fooAux s c (k.succ.succ) i = Partial.val i, from Eq.trans (ifNeg h) (ifPos h'),
have h₂ : fooAux s c k.succ i = Partial.val i, from Eq.trans (ifNeg h) (ifPos h'),
Eq.trans h₁ h₂.symm)
(λ h' : ¬ s.get i == c,
have h₁ : fooAux s c (k.succ.succ) i = fooAux s c k.succ (s.next i), from Eq.trans (ifNeg h) (ifNeg h'),
have h₂ : fooAux s c k.succ i = fooAux s c k (s.next i), from Eq.trans (ifNeg h) (ifNeg h'),
have h₃ : fooAux s c k (s.next i) ≠ Partial.bot, from h₂ ▸ ht,
have ih : fooAux s c k.succ (s.next i) = fooAux s c k (s.next i), from fooAuxEqSucc k _ h₃,
Eq.trans h₁ (Eq.trans ih h₂.symm)))
theorem fooAuxTermSucc (s : String) (c : Char) (k : Nat) (i : String.Pos)
(h₁ : terminates (fooAux s c k.succ i)) (h₂ : ¬ (s.atEnd i)) (h₃ : ¬ (s.get i == c)) : terminates (fooAux s c k (s.next i)) :=
have (fooAux s c k.succ i) = fooAux s c k (s.next i), from Eq.trans (ifNeg h₂) (ifNeg h₃),
this ▸ h₁
constant bigNat : Nat := 1000000
def foo (s : String) (c : Char) (i : String.Pos) : Partial String.Pos :=
fooAux s c bigNat i
theorem fooEq (s : String) (c : Char) (i : String.Pos) :
terminates (foo s c i) →
foo s c i = if s.atEnd i then Partial.val i
else if s.get i == c then Partial.val i
else foo s c (s.next i) :=
show terminates (fooAux s c bigNat i) → fooAux s c bigNat i = (if s.atEnd i then Partial.val i
else if s.get i == c then Partial.val i
else fooAux s c bigNat (s.next i)), from
Nat.casesOn bigNat
(λ h : fooAux s c 0 i ≠ Partial.bot, absurd rfl h)
(λ N h,
have h₁ : fooAux s c N.succ i = (if s.atEnd i then Partial.val i
else if s.get i == c then Partial.val i
else fooAux s c N (s.next i)), from rfl,
Decidable.byCases
(λ c₁ : s.atEnd i,
have aux₁ : fooAux s c N.succ i = Partial.val i, from ifPos c₁,
have aux₂ : ite (String.atEnd s i) (Partial.val i)
(ite (String.get s i == c) (Partial.val i) (fooAux s c (Nat.succ N) (String.next s i))) = Partial.val i, from ifPos c₁,
Eq.trans aux₁ aux₂.symm)
(λ c₁ : ¬ s.atEnd i,
Decidable.byCases
(λ c₂ : s.get i == c,
have aux₁ : fooAux s c N.succ i = Partial.val i, from Eq.trans (ifNeg c₁) (ifPos c₂),
have aux₂ : ite (String.atEnd s i) (Partial.val i)
(ite (String.get s i == c) (Partial.val i) (fooAux s c (Nat.succ N) (String.next s i))) = Partial.val i, from Eq.trans (ifNeg c₁) (ifPos c₂),
Eq.trans aux₁ aux₂.symm)
(λ c₂ : ¬ s.get i == c,
have h₂ : terminates (fooAux s c N (s.next i)), from fooAuxTermSucc _ _ _ _ h c₁ c₂,
have h₃ : fooAux s c N (s.next i) = fooAux s c N.succ (s.next i), from (fooAuxEqSucc _ _ _ _ h₂).symm,
h₃ ▸ h₁)))