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

refactor(library/init/core): define nat.add using equations

Browse source 
Several tests had to be patched. The new ouput is bad in several cases.
Future commits will fix that.
This commit is contained in:
Leonardo de Moura 2016-10-10 14:26:20 -07:00
parent f2a610ab52
commit 85486ad82e
8 changed files with 108 additions and 32 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
library/init/core.lean
View file

@ -343,14 +343,9 @@ def std.priority.max : num := 4294967295
namespace nat
protected def prio := num.add std.priority.default 100
protected def add (a b : nat) : nat :=
nat.rec a (λ b₁ r, nat.succ r) b
/- TODO(Leo): use the following definition as soon as we use rfl lemmas for unification
protected def add : nat → nat → nat
| a zero := a
| a (succ b) := succ (add a b)
-/
def of_pos_num : pos_num → nat
| pos_num.one := succ zero

2
tests/lean/671.lean.expected.out
View file

@ -1,2 +1,2 @@
protected definition nat.add : ℕ → ℕ → ℕ :=
λ (a b : ℕ), nat.rec a (λ (b₁ r : ℕ), nat.succ r) b
nat.add._main

12
tests/lean/def_inaccessible_issue.lean
View file

@ -4,7 +4,7 @@ set_option pp.binder_types true
inductive bv : nat → Type
| nil : bv 0
| cons : ∀ (n) (hd : bool) (tl : bv n), bv (succ n)
| cons : ∀ (n) (hd : bool) (tl : bv n), bv (n+1)
open bv
@ -14,12 +14,4 @@ definition map2 : ∀ {n}, bv n → bv n → bv n
| 0 nil nil := nil
| (n+1) (cons .n b1 v1) (cons .n b2 v2) := cons n (f b1 b2) (map2 v1 v2)
check map2._main.equations.eqn_2
/- defining function again without simplifying the type of automatically generated lemmas -/
definition map2' : ∀ {n}, bv n → bv n → bv n
| 0 nil nil := nil
| (n+1) (cons .n b1 v1) (cons .n b2 v2) := cons n (f b1 b2) (map2' v1 v2)
check map2'._main.equations.eqn_2
check map2.equations.eqn_2

13
tests/lean/def_inaccessible_issue.lean.expected.out
View file

@ -1,10 +1,3 @@
map2._main.equations.eqn_2 :
∀ (f : bool → bool → bool) (n : ℕ) (b1 : bool) (v1 : bv (nat.rec n (λ (b₁ r : ℕ), succ r) 0)) (b2 : bool)
(v2 : bv (nat.rec n (λ (b₁ r : ℕ), succ r) 0)),
map2._main f (cons (nat.rec n (λ (b₁ r : ℕ), succ r) 0) b1 v1)
(cons (nat.rec n (λ (b₁ r : ℕ), succ r) 0) b2 v2) = cons n (f b1 b2) (map2._main f v1 v2)
map2'._main.equations.eqn_2 :
∀ (f : bool → bool → bool) (n : ℕ) (b1 : bool) (v1 : bv (nat.rec n (λ (b₁ r : ℕ), succ r) 0)) (b2 : bool)
(v2 : bv (nat.rec n (λ (b₁ r : ℕ), succ r) 0)),
map2'._main f (cons (nat.rec n (λ (b₁ r : ℕ), succ r) 0) b1 v1)
(cons (nat.rec n (λ (b₁ r : ℕ), succ r) 0) b2 v2) = cons n (f b1 b2) (map2'._main f v1 v2)
map2.equations.eqn_2 :
∀ (f : bool → bool → bool) (n : ℕ) (b1 : bool) (v1 : bv n) (b2 : bool) (v2 : bv n),
map2 f (cons n b1 v1) (cons n b2 v2) = cons n (f b1 b2) (map2 f v1 v2)

2
tests/lean/unfold_crash.lean.expected.out
View file

@ -1,3 +1,3 @@
a b : ℕ,
H : a = succ b
⊢ a = succ b
⊢ a = add._main b 1

32
tests/lean/whnf.lean.expected.out
View file

@ -1,4 +1,32 @@
succ (nat.rec 2 (λ (b₁ r : ℕ), succ r) 0)
succ
(prod.fst
(prod.fst
(nat.rec
(λ (a : ℕ),
nat.cases_on 0 (λ (_F : nat.below 0), a)
(λ (a_1 : ℕ) (_F : nat.below (succ a_1)), succ (prod.fst (prod.fst _F) a))
poly_unit.star, poly_unit.star)
(λ (a : ℕ) (ih_1 : (ℕ → ℕ) × nat.below a),
(λ (a_1 : ℕ),
nat.cases_on (succ a) (λ (_F : nat.below 0), a_1)
(λ (a : ℕ) (_F : nat.below (succ a)), succ (prod.fst (prod.fst _F) a_1))
(ih_1, poly_unit.star), ih_1, poly_unit.star))
0, poly_unit.star))
2)
3
succ (nat.rec a (λ (b₁ r : ℕ), succ r) 0)
succ
(prod.fst
(prod.fst
(nat.rec
(λ (a : ℕ),
nat.cases_on 0 (λ (_F : nat.below 0), a)
(λ (a_1 : ℕ) (_F : nat.below (succ a_1)), succ (prod.fst (prod.fst _F) a))
poly_unit.star, poly_unit.star)
(λ (a : ℕ) (ih_1 : (ℕ → ℕ) × nat.below a),
(λ (a_1 : ℕ),
nat.cases_on (succ a) (λ (_F : nat.below 0), a_1)
(λ (a : ℕ) (_F : nat.below (succ a)), succ (prod.fst (prod.fst _F) a_1))
(ih_1, poly_unit.star), ih_1, poly_unit.star))
0, poly_unit.star))
a)
succ a

16
tests/lean/whnf_cache_bug.lean.expected.out
View file

@ -1,2 +1,16 @@
?m_1
nat.succ (nat.rec 1 (λ (b₁ r : ℕ), nat.succ r) 0)
nat.succ
(prod.fst
(prod.fst
(nat.rec
(λ (a : ℕ),
nat.cases_on 0 (λ (_F : nat.below 0), a)
(λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a))
poly_unit.star, poly_unit.star)
(λ (a : ℕ) (ih_1 : (ℕ → ℕ) × nat.below a),
(λ (a_1 : ℕ),
nat.cases_on (nat.succ a) (λ (_F : nat.below 0), a_1)
(λ (a : ℕ) (_F : nat.below (nat.succ a)), nat.succ (prod.fst (prod.fst _F) a_1))
(ih_1, poly_unit.star), ih_1, poly_unit.star))
0, poly_unit.star))
1)

58
tests/lean/whnf_core1.lean.expected.out
View file

@ -1,4 +1,58 @@
nat.succ (nat.rec a (λ (b₁ r : ℕ), nat.succ r) (nat.rec 1 (λ (b₁ r : ℕ), nat.succ r) 0))
nat.succ (nat.rec a (λ (b₁ r : ℕ), nat.succ r) (nat.rec 1 (λ (b₁ r : ℕ), nat.succ r) 0))
nat.succ
(prod.fst
(prod.fst
(nat.rec
(λ (a : ℕ),
nat.cases_on 0 (λ (_F : nat.below 0), a)
(λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a))
poly_unit.star, poly_unit.star)
(λ (a : ℕ) (ih_1 : (ℕ → ℕ) × nat.below a),
(λ (a_1 : ℕ),
nat.cases_on (nat.succ a) (λ (_F : nat.below 0), a_1)
(λ (a : ℕ) (_F : nat.below (nat.succ a)), nat.succ (prod.fst (prod.fst _F) a_1))
(ih_1, poly_unit.star), ih_1, poly_unit.star))
(prod.fst
(prod.fst
(nat.rec
(λ (a : ℕ),
nat.cases_on 0 (λ (_F : nat.below 0), a)
(λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a))
poly_unit.star, poly_unit.star)
(λ (a : ℕ) (ih_1 : (ℕ → ℕ) × nat.below a),
(λ (a_1 : ℕ),
nat.cases_on (nat.succ a) (λ (_F : nat.below 0), a_1)
(λ (a : ℕ) (_F : nat.below (nat.succ a)), nat.succ (prod.fst (prod.fst _F) a_1))
(ih_1, poly_unit.star), ih_1, poly_unit.star))
0, poly_unit.star))
1), poly_unit.star))
a)
nat.succ
(prod.fst
(prod.fst
(nat.rec
(λ (a : ℕ),
nat.cases_on 0 (λ (_F : nat.below 0), a)
(λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a))
poly_unit.star, poly_unit.star)
(λ (a : ℕ) (ih_1 : (ℕ → ℕ) × nat.below a),
(λ (a_1 : ℕ),
nat.cases_on (nat.succ a) (λ (_F : nat.below 0), a_1)
(λ (a : ℕ) (_F : nat.below (nat.succ a)), nat.succ (prod.fst (prod.fst _F) a_1))
(ih_1, poly_unit.star), ih_1, poly_unit.star))
(prod.fst
(prod.fst
(nat.rec
(λ (a : ℕ),
nat.cases_on 0 (λ (_F : nat.below 0), a)
(λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ (prod.fst (prod.fst _F) a))
poly_unit.star, poly_unit.star)
(λ (a : ℕ) (ih_1 : (ℕ → ℕ) × nat.below a),
(λ (a_1 : ℕ),
nat.cases_on (nat.succ a) (λ (_F : nat.below 0), a_1)
(λ (a : ℕ) (_F : nat.below (nat.succ a)), nat.succ (prod.fst (prod.fst _F) a_1))
(ih_1, poly_unit.star), ih_1, poly_unit.star))
0, poly_unit.star))
1), poly_unit.star))
a)
f a
a + 2