feat(frontends/lean): ML-like notation for match and recursive equations
This commit is contained in:
Leonardo de Moura
parent
3c24461e51
commit
5ca52d81ec
53 changed files with 420 additions and 408 deletions
|
|
@ -17,14 +17,14 @@ namespace sigma
|
|||
{a a' a'' : A} {b b₁ b₂ : B a} {b' : B a'} {b'' : B a''} {u v w : Σa, B a}
|
||||
|
||||
-- sigma.eta is already used for the eta rule for strict equality
|
||||
protected definition eta : Π (u : Σa, B a), ⟨u.1 , u.2⟩ = u,
|
||||
eta ⟨u₁, u₂⟩ := idp
|
||||
protected definition eta : Π (u : Σa, B a), ⟨u.1 , u.2⟩ = u
|
||||
| eta ⟨u₁, u₂⟩ := idp
|
||||
|
||||
definition eta2 : Π (u : Σa b, C a b), ⟨u.1, u.2.1, u.2.2⟩ = u,
|
||||
eta2 ⟨u₁, u₂, u₃⟩ := idp
|
||||
definition eta2 : Π (u : Σa b, C a b), ⟨u.1, u.2.1, u.2.2⟩ = u
|
||||
| eta2 ⟨u₁, u₂, u₃⟩ := idp
|
||||
|
||||
definition eta3 : Π (u : Σa b c, D a b c), ⟨u.1, u.2.1, u.2.2.1, u.2.2.2⟩ = u,
|
||||
eta3 ⟨u₁, u₂, u₃, u₄⟩ := idp
|
||||
definition eta3 : Π (u : Σa b c, D a b c), ⟨u.1, u.2.1, u.2.2.1, u.2.2.2⟩ = u
|
||||
| eta3 ⟨u₁, u₂, u₃, u₄⟩ := idp
|
||||
|
||||
definition dpair_eq_dpair (p : a = a') (q : p ▹ b = b') : ⟨a, b⟩ = ⟨a', b'⟩ :=
|
||||
by cases p; cases q; apply idp
|
||||
|
|
@ -68,12 +68,12 @@ namespace sigma
|
|||
|
||||
/- the uncurried version of sigma_eq. We will prove that this is an equivalence -/
|
||||
|
||||
definition sigma_eq_uncurried : Π (pq : Σ(p : pr1 u = pr1 v), p ▹ (pr2 u) = pr2 v), u = v,
|
||||
sigma_eq_uncurried ⟨pq₁, pq₂⟩ := sigma_eq pq₁ pq₂
|
||||
definition sigma_eq_uncurried : Π (pq : Σ(p : pr1 u = pr1 v), p ▹ (pr2 u) = pr2 v), u = v
|
||||
| sigma_eq_uncurried ⟨pq₁, pq₂⟩ := sigma_eq pq₁ pq₂
|
||||
|
||||
definition dpair_sigma_eq_uncurried : Π (pq : Σ(p : u.1 = v.1), p ▹ u.2 = v.2),
|
||||
sigma.mk (sigma_eq_uncurried pq)..1 (sigma_eq_uncurried pq)..2 = pq,
|
||||
dpair_sigma_eq_uncurried ⟨pq₁, pq₂⟩ := dpair_sigma_eq pq₁ pq₂
|
||||
sigma.mk (sigma_eq_uncurried pq)..1 (sigma_eq_uncurried pq)..2 = pq
|
||||
| dpair_sigma_eq_uncurried ⟨pq₁, pq₂⟩ := dpair_sigma_eq pq₁ pq₂
|
||||
|
||||
definition sigma_eq_pr1_uncurried (pq : Σ(p : u.1 = v.1), p ▹ u.2 = v.2)
|
||||
: (sigma_eq_uncurried pq)..1 = pq.1 :=
|
||||
|
|
|
|||
|
|
@ -15,9 +15,9 @@ fz : Π n, fin (succ n),
|
|||
fs : Π {n}, fin n → fin (succ n)
|
||||
|
||||
namespace fin
|
||||
definition to_nat : Π {n}, fin n → nat,
|
||||
@to_nat ⌞n+1⌟ (fz n) := zero,
|
||||
@to_nat ⌞n+1⌟ (fs f) := succ (to_nat f)
|
||||
definition to_nat : Π {n}, fin n → nat
|
||||
| @to_nat ⌞n+1⌟ (fz n) := zero
|
||||
| @to_nat ⌞n+1⌟ (fs f) := succ (to_nat f)
|
||||
|
||||
theorem to_nat_fz (n : nat) : to_nat (fz n) = zero :=
|
||||
rfl
|
||||
|
|
@ -25,17 +25,17 @@ namespace fin
|
|||
theorem to_nat_fs {n : nat} (f : fin n) : to_nat (fs f) = succ (to_nat f) :=
|
||||
rfl
|
||||
|
||||
theorem to_nat_lt : Π {n} (f : fin n), to_nat f < n,
|
||||
to_nat_lt (fz n) := calc
|
||||
to_nat (fz n) = 0 : rfl
|
||||
... < n+1 : succ_pos n,
|
||||
to_nat_lt (@fs n f) := calc
|
||||
to_nat (fs f) = (to_nat f)+1 : rfl
|
||||
... < n+1 : succ_lt_succ (to_nat_lt f)
|
||||
theorem to_nat_lt : Π {n} (f : fin n), to_nat f < n
|
||||
| to_nat_lt (fz n) := calc
|
||||
to_nat (fz n) = 0 : rfl
|
||||
... < n+1 : succ_pos n
|
||||
| to_nat_lt (@fs n f) := calc
|
||||
to_nat (fs f) = (to_nat f)+1 : rfl
|
||||
... < n+1 : succ_lt_succ (to_nat_lt f)
|
||||
|
||||
definition lift : Π {n : nat}, fin n → Π (m : nat), fin (m + n),
|
||||
@lift ⌞n+1⌟ (fz n) m := fz (m + n),
|
||||
@lift ⌞n+1⌟ (@fs n f) m := fs (lift f m)
|
||||
definition lift : Π {n : nat}, fin n → Π (m : nat), fin (m + n)
|
||||
| @lift ⌞n+1⌟ (fz n) m := fz (m + n)
|
||||
| @lift ⌞n+1⌟ (@fs n f) m := fs (lift f m)
|
||||
|
||||
theorem lift_fz (n m : nat) : lift (fz n) m = fz (m + n) :=
|
||||
rfl
|
||||
|
|
@ -43,18 +43,18 @@ namespace fin
|
|||
theorem lift_fs {n : nat} (f : fin n) (m : nat) : lift (fs f) m = fs (lift f m) :=
|
||||
rfl
|
||||
|
||||
theorem to_nat_lift : ∀ {n : nat} (f : fin n) (m : nat), to_nat f = to_nat (lift f m),
|
||||
to_nat_lift (fz n) m := rfl,
|
||||
to_nat_lift (@fs n f) m := calc
|
||||
theorem to_nat_lift : ∀ {n : nat} (f : fin n) (m : nat), to_nat f = to_nat (lift f m)
|
||||
| to_nat_lift (fz n) m := rfl
|
||||
| to_nat_lift (@fs n f) m := calc
|
||||
to_nat (fs f) = (to_nat f) + 1 : rfl
|
||||
... = (to_nat (lift f m)) + 1 : to_nat_lift f
|
||||
... = to_nat (lift (fs f) m) : rfl
|
||||
|
||||
definition of_nat : Π (p : nat) (n : nat), p < n → fin n,
|
||||
of_nat 0 0 h := absurd h (not_lt_zero zero),
|
||||
of_nat 0 (n+1) h := fz n,
|
||||
of_nat (p+1) 0 h := absurd h (not_lt_zero (succ p)),
|
||||
of_nat (p+1) (n+1) h := fs (of_nat p n (lt_of_succ_lt_succ h))
|
||||
definition of_nat : Π (p : nat) (n : nat), p < n → fin n
|
||||
| of_nat 0 0 h := absurd h (not_lt_zero zero)
|
||||
| of_nat 0 (n+1) h := fz n
|
||||
| of_nat (p+1) 0 h := absurd h (not_lt_zero (succ p))
|
||||
| of_nat (p+1) (n+1) h := fs (of_nat p n (lt_of_succ_lt_succ h))
|
||||
|
||||
theorem of_nat_zero_succ (n : nat) (h : 0 < n+1) : of_nat 0 (n+1) h = fz n :=
|
||||
rfl
|
||||
|
|
@ -63,19 +63,19 @@ namespace fin
|
|||
of_nat (p+1) (n+1) h = fs (of_nat p n (lt_of_succ_lt_succ h)) :=
|
||||
rfl
|
||||
|
||||
theorem to_nat_of_nat : ∀ (p : nat) (n : nat) (h : p < n), to_nat (of_nat p n h) = p,
|
||||
to_nat_of_nat 0 0 h := absurd h (not_lt_zero 0),
|
||||
to_nat_of_nat 0 (n+1) h := rfl,
|
||||
to_nat_of_nat (p+1) 0 h := absurd h (not_lt_zero (p+1)),
|
||||
to_nat_of_nat (p+1) (n+1) h := calc
|
||||
to_nat (of_nat (p+1) (n+1) h)
|
||||
= succ (to_nat (of_nat p n _)) : rfl
|
||||
... = succ p : {to_nat_of_nat p n _}
|
||||
theorem to_nat_of_nat : ∀ (p : nat) (n : nat) (h : p < n), to_nat (of_nat p n h) = p
|
||||
| to_nat_of_nat 0 0 h := absurd h (not_lt_zero 0)
|
||||
| to_nat_of_nat 0 (n+1) h := rfl
|
||||
| to_nat_of_nat (p+1) 0 h := absurd h (not_lt_zero (p+1))
|
||||
| to_nat_of_nat (p+1) (n+1) h := calc
|
||||
to_nat (of_nat (p+1) (n+1) h)
|
||||
= succ (to_nat (of_nat p n _)) : rfl
|
||||
... = succ p : {to_nat_of_nat p n _}
|
||||
|
||||
theorem of_nat_to_nat : ∀ {n : nat} (f : fin n) (h : to_nat f < n), of_nat (to_nat f) n h = f,
|
||||
of_nat_to_nat (fz n) h := rfl,
|
||||
of_nat_to_nat (@fs n f) h := calc
|
||||
of_nat (to_nat (fs f)) (succ n) h = fs (of_nat (to_nat f) n _) : rfl
|
||||
... = fs f : {of_nat_to_nat f _}
|
||||
theorem of_nat_to_nat : ∀ {n : nat} (f : fin n) (h : to_nat f < n), of_nat (to_nat f) n h = f
|
||||
| of_nat_to_nat (fz n) h := rfl
|
||||
| of_nat_to_nat (@fs n f) h := calc
|
||||
of_nat (to_nat (fs f)) (succ n) h = fs (of_nat (to_nat f) n _) : rfl
|
||||
... = fs f : {of_nat_to_nat f _}
|
||||
|
||||
end fin
|
||||
|
|
|
|||
|
|
@ -24,8 +24,8 @@ namespace int
|
|||
definition divide (a b : ℤ) : ℤ :=
|
||||
sign b *
|
||||
(match a with
|
||||
of_nat m := #nat m div (nat_abs b),
|
||||
-[ m +1] := -[ (#nat m div (nat_abs b)) +1]
|
||||
| of_nat m := #nat m div (nat_abs b)
|
||||
| -[ m +1] := -[ (#nat m div (nat_abs b)) +1]
|
||||
end)
|
||||
|
||||
notation a div b := divide a b
|
||||
|
|
|
|||
|
|
@ -24,9 +24,9 @@ variable {T : Type}
|
|||
|
||||
/- append -/
|
||||
|
||||
definition append : list T → list T → list T,
|
||||
append nil l := l,
|
||||
append (h :: s) t := h :: (append s t)
|
||||
definition append : list T → list T → list T
|
||||
| append nil l := l
|
||||
| append (h :: s) t := h :: (append s t)
|
||||
|
||||
notation l₁ ++ l₂ := append l₁ l₂
|
||||
|
||||
|
|
@ -34,66 +34,66 @@ theorem append_nil_left (t : list T) : nil ++ t = t
|
|||
|
||||
theorem append_cons (x : T) (s t : list T) : (x::s) ++ t = x::(s ++ t)
|
||||
|
||||
theorem append_nil_right : ∀ (t : list T), t ++ nil = t,
|
||||
append_nil_right nil := rfl,
|
||||
append_nil_right (a :: l) := calc
|
||||
theorem append_nil_right : ∀ (t : list T), t ++ nil = t
|
||||
| append_nil_right nil := rfl
|
||||
| append_nil_right (a :: l) := calc
|
||||
(a :: l) ++ nil = a :: (l ++ nil) : rfl
|
||||
... = a :: l : append_nil_right l
|
||||
|
||||
|
||||
theorem append.assoc : ∀ (s t u : list T), s ++ t ++ u = s ++ (t ++ u),
|
||||
append.assoc nil t u := rfl,
|
||||
append.assoc (a :: l) t u := calc
|
||||
theorem append.assoc : ∀ (s t u : list T), s ++ t ++ u = s ++ (t ++ u)
|
||||
| append.assoc nil t u := rfl
|
||||
| append.assoc (a :: l) t u := calc
|
||||
(a :: l) ++ t ++ u = a :: (l ++ t ++ u) : rfl
|
||||
... = a :: (l ++ (t ++ u)) : append.assoc
|
||||
... = (a :: l) ++ (t ++ u) : rfl
|
||||
|
||||
/- length -/
|
||||
|
||||
definition length : list T → nat,
|
||||
length nil := 0,
|
||||
length (a :: l) := length l + 1
|
||||
definition length : list T → nat
|
||||
| length nil := 0
|
||||
| length (a :: l) := length l + 1
|
||||
|
||||
theorem length_nil : length (@nil T) = 0
|
||||
|
||||
theorem length_cons (x : T) (t : list T) : length (x::t) = length t + 1
|
||||
|
||||
theorem length_append : ∀ (s t : list T), length (s ++ t) = length s + length t,
|
||||
length_append nil t := calc
|
||||
length (nil ++ t) = length t : rfl
|
||||
... = length nil + length t : zero_add,
|
||||
length_append (a :: s) t := calc
|
||||
length (a :: s ++ t) = length (s ++ t) + 1 : rfl
|
||||
... = length s + length t + 1 : length_append
|
||||
... = (length s + 1) + length t : add.succ_left
|
||||
... = length (a :: s) + length t : rfl
|
||||
theorem length_append : ∀ (s t : list T), length (s ++ t) = length s + length t
|
||||
| length_append nil t := calc
|
||||
length (nil ++ t) = length t : rfl
|
||||
... = length nil + length t : zero_add
|
||||
| length_append (a :: s) t := calc
|
||||
length (a :: s ++ t) = length (s ++ t) + 1 : rfl
|
||||
... = length s + length t + 1 : length_append
|
||||
... = (length s + 1) + length t : add.succ_left
|
||||
... = length (a :: s) + length t : rfl
|
||||
|
||||
-- add_rewrite length_nil length_cons
|
||||
|
||||
/- concat -/
|
||||
|
||||
definition concat : Π (x : T), list T → list T,
|
||||
concat a nil := [a],
|
||||
concat a (b :: l) := b :: concat a l
|
||||
definition concat : Π (x : T), list T → list T
|
||||
| concat a nil := [a]
|
||||
| concat a (b :: l) := b :: concat a l
|
||||
|
||||
theorem concat_nil (x : T) : concat x nil = [x]
|
||||
|
||||
theorem concat_cons (x y : T) (l : list T) : concat x (y::l) = y::(concat x l)
|
||||
|
||||
theorem concat_eq_append (a : T) : ∀ (l : list T), concat a l = l ++ [a],
|
||||
concat_eq_append nil := rfl,
|
||||
concat_eq_append (b :: l) := calc
|
||||
concat a (b :: l) = b :: (concat a l) : rfl
|
||||
... = b :: (l ++ [a]) : concat_eq_append
|
||||
... = (b :: l) ++ [a] : rfl
|
||||
theorem concat_eq_append (a : T) : ∀ (l : list T), concat a l = l ++ [a]
|
||||
| concat_eq_append nil := rfl
|
||||
| concat_eq_append (b :: l) := calc
|
||||
concat a (b :: l) = b :: (concat a l) : rfl
|
||||
... = b :: (l ++ [a]) : concat_eq_append
|
||||
... = (b :: l) ++ [a] : rfl
|
||||
|
||||
-- add_rewrite append_nil append_cons
|
||||
|
||||
/- reverse -/
|
||||
|
||||
definition reverse : list T → list T,
|
||||
reverse nil := nil,
|
||||
reverse (a :: l) := concat a (reverse l)
|
||||
definition reverse : list T → list T
|
||||
| reverse nil := nil
|
||||
| reverse (a :: l) := concat a (reverse l)
|
||||
|
||||
theorem reverse_nil : reverse (@nil T) = nil
|
||||
|
||||
|
|
@ -101,27 +101,27 @@ theorem reverse_cons (x : T) (l : list T) : reverse (x::l) = concat x (reverse l
|
|||
|
||||
theorem reverse_singleton (x : T) : reverse [x] = [x]
|
||||
|
||||
theorem reverse_append : ∀ (s t : list T), reverse (s ++ t) = (reverse t) ++ (reverse s),
|
||||
reverse_append nil t2 := calc
|
||||
reverse (nil ++ t2) = reverse t2 : rfl
|
||||
... = (reverse t2) ++ nil : append_nil_right
|
||||
... = (reverse t2) ++ (reverse nil) : {reverse_nil⁻¹},
|
||||
reverse_append (a2 :: s2) t2 := calc
|
||||
reverse ((a2 :: s2) ++ t2) = concat a2 (reverse (s2 ++ t2)) : rfl
|
||||
... = concat a2 (reverse t2 ++ reverse s2) : reverse_append
|
||||
... = (reverse t2 ++ reverse s2) ++ [a2] : concat_eq_append
|
||||
... = reverse t2 ++ (reverse s2 ++ [a2]) : append.assoc
|
||||
... = reverse t2 ++ concat a2 (reverse s2) : concat_eq_append
|
||||
... = reverse t2 ++ reverse (a2 :: s2) : rfl
|
||||
theorem reverse_append : ∀ (s t : list T), reverse (s ++ t) = (reverse t) ++ (reverse s)
|
||||
| reverse_append nil t2 := calc
|
||||
reverse (nil ++ t2) = reverse t2 : rfl
|
||||
... = (reverse t2) ++ nil : append_nil_right
|
||||
... = (reverse t2) ++ (reverse nil) : {reverse_nil⁻¹}
|
||||
| reverse_append (a2 :: s2) t2 := calc
|
||||
reverse ((a2 :: s2) ++ t2) = concat a2 (reverse (s2 ++ t2)) : rfl
|
||||
... = concat a2 (reverse t2 ++ reverse s2) : reverse_append
|
||||
... = (reverse t2 ++ reverse s2) ++ [a2] : concat_eq_append
|
||||
... = reverse t2 ++ (reverse s2 ++ [a2]) : append.assoc
|
||||
... = reverse t2 ++ concat a2 (reverse s2) : concat_eq_append
|
||||
... = reverse t2 ++ reverse (a2 :: s2) : rfl
|
||||
|
||||
theorem reverse_reverse : ∀ (l : list T), reverse (reverse l) = l,
|
||||
reverse_reverse nil := rfl,
|
||||
reverse_reverse (a :: l) := calc
|
||||
reverse (reverse (a :: l)) = reverse (concat a (reverse l)) : rfl
|
||||
... = reverse (reverse l ++ [a]) : concat_eq_append
|
||||
... = reverse [a] ++ reverse (reverse l) : reverse_append
|
||||
... = reverse [a] ++ l : reverse_reverse
|
||||
... = a :: l : rfl
|
||||
theorem reverse_reverse : ∀ (l : list T), reverse (reverse l) = l
|
||||
| reverse_reverse nil := rfl
|
||||
| reverse_reverse (a :: l) := calc
|
||||
reverse (reverse (a :: l)) = reverse (concat a (reverse l)) : rfl
|
||||
... = reverse (reverse l ++ [a]) : concat_eq_append
|
||||
... = reverse [a] ++ reverse (reverse l) : reverse_append
|
||||
... = reverse [a] ++ l : reverse_reverse
|
||||
... = a :: l : rfl
|
||||
|
||||
theorem concat_eq_reverse_cons (x : T) (l : list T) : concat x l = reverse (x :: reverse l) :=
|
||||
calc
|
||||
|
|
@ -130,9 +130,9 @@ calc
|
|||
|
||||
/- head and tail -/
|
||||
|
||||
definition head [h : inhabited T] : list T → T,
|
||||
head nil := arbitrary T,
|
||||
head (a :: l) := a
|
||||
definition head [h : inhabited T] : list T → T
|
||||
| head nil := arbitrary T
|
||||
| head (a :: l) := a
|
||||
|
||||
theorem head_cons [h : inhabited T] (a : T) (l : list T) : head (a::l) = a
|
||||
|
||||
|
|
@ -145,9 +145,9 @@ list.cases_on s
|
|||
... = x : head_cons
|
||||
... = head (x::s) : rfl)
|
||||
|
||||
definition tail : list T → list T,
|
||||
tail nil := nil,
|
||||
tail (a :: l) := l
|
||||
definition tail : list T → list T
|
||||
| tail nil := nil
|
||||
| tail (a :: l) := l
|
||||
|
||||
theorem tail_nil : tail (@nil T) = nil
|
||||
|
||||
|
|
@ -160,9 +160,9 @@ list.cases_on l
|
|||
|
||||
/- list membership -/
|
||||
|
||||
definition mem : T → list T → Prop,
|
||||
mem a nil := false,
|
||||
mem a (b :: l) := a = b ∨ mem a l
|
||||
definition mem : T → list T → Prop
|
||||
| mem a nil := false
|
||||
| mem a (b :: l) := a = b ∨ mem a l
|
||||
|
||||
notation e ∈ s := mem e s
|
||||
|
||||
|
|
@ -246,9 +246,9 @@ section
|
|||
variable [H : decidable_eq T]
|
||||
include H
|
||||
|
||||
definition find : T → list T → nat,
|
||||
find a nil := 0,
|
||||
find a (b :: l) := if a = b then 0 else succ (find a l)
|
||||
definition find : T → list T → nat
|
||||
| find a nil := 0
|
||||
| find a (b :: l) := if a = b then 0 else succ (find a l)
|
||||
|
||||
theorem find_nil (x : T) : find x nil = 0
|
||||
|
||||
|
|
@ -271,10 +271,10 @@ end
|
|||
|
||||
/- nth element -/
|
||||
|
||||
definition nth [h : inhabited T] : list T → nat → T,
|
||||
nth nil n := arbitrary T,
|
||||
nth (a :: l) 0 := a,
|
||||
nth (a :: l) (n+1) := nth l n
|
||||
definition nth [h : inhabited T] : list T → nat → T
|
||||
| nth nil n := arbitrary T
|
||||
| nth (a :: l) 0 := a
|
||||
| nth (a :: l) (n+1) := nth l n
|
||||
|
||||
theorem nth_zero [h : inhabited T] (a : T) (l : list T) : nth (a :: l) 0 = a
|
||||
|
||||
|
|
|
|||
|
|
@ -13,7 +13,7 @@ set_option structure.proj_mk_thm true
|
|||
structure subtype {A : Type} (P : A → Prop) :=
|
||||
tag :: (elt_of : A) (has_property : P elt_of)
|
||||
|
||||
notation `{` binders:55 `|` r:(scoped:1 P, subtype P) `}` := r
|
||||
notation `{` binders `|` r:(scoped:1 P, subtype P) `}` := r
|
||||
|
||||
namespace subtype
|
||||
variables {A : Type} {P : A → Prop}
|
||||
|
|
|
|||
|
|
@ -39,17 +39,17 @@ namespace sum
|
|||
protected definition is_inhabited_right [instance] [h : inhabited B] : inhabited (A + B) :=
|
||||
inhabited.mk (inr (default B))
|
||||
|
||||
protected definition has_decidable_eq [instance] [h₁ : decidable_eq A] [h₂ : decidable_eq B] : ∀ s₁ s₂ : A + B, decidable (s₁ = s₂),
|
||||
has_decidable_eq (inl a₁) (inl a₂) :=
|
||||
protected definition has_decidable_eq [instance] [h₁ : decidable_eq A] [h₂ : decidable_eq B] : ∀ s₁ s₂ : A + B, decidable (s₁ = s₂)
|
||||
| has_decidable_eq (inl a₁) (inl a₂) :=
|
||||
match h₁ a₁ a₂ with
|
||||
decidable.inl hp := decidable.inl (hp ▸ rfl),
|
||||
decidable.inr hn := decidable.inr (λ he, absurd (inl_inj he) hn)
|
||||
end,
|
||||
has_decidable_eq (inl a₁) (inr b₂) := decidable.inr (λ e, sum.no_confusion e),
|
||||
has_decidable_eq (inr b₁) (inl a₂) := decidable.inr (λ e, sum.no_confusion e),
|
||||
has_decidable_eq (inr b₁) (inr b₂) :=
|
||||
| decidable.inl hp := decidable.inl (hp ▸ rfl)
|
||||
| decidable.inr hn := decidable.inr (λ he, absurd (inl_inj he) hn)
|
||||
end
|
||||
| has_decidable_eq (inl a₁) (inr b₂) := decidable.inr (λ e, sum.no_confusion e)
|
||||
| has_decidable_eq (inr b₁) (inl a₂) := decidable.inr (λ e, sum.no_confusion e)
|
||||
| has_decidable_eq (inr b₁) (inr b₂) :=
|
||||
match h₂ b₁ b₂ with
|
||||
decidable.inl hp := decidable.inl (hp ▸ rfl),
|
||||
decidable.inr hn := decidable.inr (λ he, absurd (inr_inj he) hn)
|
||||
| decidable.inl hp := decidable.inl (hp ▸ rfl)
|
||||
| decidable.inr hn := decidable.inr (λ he, absurd (inr_inj he) hn)
|
||||
end
|
||||
end sum
|
||||
|
|
|
|||
|
|
@ -18,18 +18,18 @@ namespace vector
|
|||
|
||||
variables {A B C : Type}
|
||||
|
||||
protected definition is_inhabited [instance] [h : inhabited A] : ∀ (n : nat), inhabited (vector A n),
|
||||
is_inhabited 0 := inhabited.mk nil,
|
||||
is_inhabited (n+1) := inhabited.mk (inhabited.value h :: inhabited.value (is_inhabited n))
|
||||
protected definition is_inhabited [instance] [h : inhabited A] : ∀ (n : nat), inhabited (vector A n)
|
||||
| is_inhabited 0 := inhabited.mk nil
|
||||
| is_inhabited (n+1) := inhabited.mk (inhabited.value h :: inhabited.value (is_inhabited n))
|
||||
|
||||
theorem vector0_eq_nil : ∀ (v : vector A 0), v = nil,
|
||||
vector0_eq_nil nil := rfl
|
||||
theorem vector0_eq_nil : ∀ (v : vector A 0), v = nil
|
||||
| vector0_eq_nil nil := rfl
|
||||
|
||||
definition head : Π {n : nat}, vector A (succ n) → A,
|
||||
head (a::v) := a
|
||||
definition head : Π {n : nat}, vector A (succ n) → A
|
||||
| head (a::v) := a
|
||||
|
||||
definition tail : Π {n : nat}, vector A (succ n) → vector A n,
|
||||
tail (a::v) := v
|
||||
definition tail : Π {n : nat}, vector A (succ n) → vector A n
|
||||
| tail (a::v) := v
|
||||
|
||||
theorem head_cons {n : nat} (h : A) (t : vector A n) : head (h :: t) = h :=
|
||||
rfl
|
||||
|
|
@ -37,12 +37,12 @@ namespace vector
|
|||
theorem tail_cons {n : nat} (h : A) (t : vector A n) : tail (h :: t) = t :=
|
||||
rfl
|
||||
|
||||
theorem eta : ∀ {n : nat} (v : vector A (succ n)), head v :: tail v = v,
|
||||
eta (a::v) := rfl
|
||||
theorem eta : ∀ {n : nat} (v : vector A (succ n)), head v :: tail v = v
|
||||
| eta (a::v) := rfl
|
||||
|
||||
definition last : Π {n : nat}, vector A (succ n) → A,
|
||||
last (a::nil) := a,
|
||||
last (a::v) := last v
|
||||
definition last : Π {n : nat}, vector A (succ n) → A
|
||||
| last (a::nil) := a
|
||||
| last (a::v) := last v
|
||||
|
||||
theorem last_singleton (a : A) : last (a :: nil) = a :=
|
||||
rfl
|
||||
|
|
@ -50,20 +50,20 @@ namespace vector
|
|||
theorem last_cons {n : nat} (a : A) (v : vector A (succ n)) : last (a :: v) = last v :=
|
||||
rfl
|
||||
|
||||
definition const : Π (n : nat), A → vector A n,
|
||||
const 0 a := nil,
|
||||
const (succ n) a := a :: const n a
|
||||
definition const : Π (n : nat), A → vector A n
|
||||
| const 0 a := nil
|
||||
| const (succ n) a := a :: const n a
|
||||
|
||||
theorem head_const (n : nat) (a : A) : head (const (succ n) a) = a :=
|
||||
rfl
|
||||
|
||||
theorem last_const : ∀ (n : nat) (a : A), last (const (succ n) a) = a,
|
||||
last_const 0 a := rfl,
|
||||
last_const (succ n) a := last_const n a
|
||||
theorem last_const : ∀ (n : nat) (a : A), last (const (succ n) a) = a
|
||||
| last_const 0 a := rfl
|
||||
| last_const (succ n) a := last_const n a
|
||||
|
||||
definition map (f : A → B) : Π {n : nat}, vector A n → vector B n,
|
||||
map nil := nil,
|
||||
map (a::v) := f a :: map v
|
||||
definition map (f : A → B) : Π {n : nat}, vector A n → vector B n
|
||||
| map nil := nil
|
||||
| map (a::v) := f a :: map v
|
||||
|
||||
theorem map_nil (f : A → B) : map f nil = nil :=
|
||||
rfl
|
||||
|
|
@ -71,9 +71,9 @@ namespace vector
|
|||
theorem map_cons {n : nat} (f : A → B) (h : A) (t : vector A n) : map f (h :: t) = f h :: map f t :=
|
||||
rfl
|
||||
|
||||
definition map2 (f : A → B → C) : Π {n : nat}, vector A n → vector B n → vector C n,
|
||||
map2 nil nil := nil,
|
||||
map2 (a::va) (b::vb) := f a b :: map2 va vb
|
||||
definition map2 (f : A → B → C) : Π {n : nat}, vector A n → vector B n → vector C n
|
||||
| map2 nil nil := nil
|
||||
| map2 (a::va) (b::vb) := f a b :: map2 va vb
|
||||
|
||||
theorem map2_nil (f : A → B → C) : map2 f nil nil = nil :=
|
||||
rfl
|
||||
|
|
@ -83,9 +83,9 @@ namespace vector
|
|||
rfl
|
||||
|
||||
-- Remark: why do we need to provide indices?
|
||||
definition append : Π {n m : nat}, vector A n → vector A m → vector A (n ⊕ m),
|
||||
@append 0 m nil w := w,
|
||||
@append (succ n) m (a::v) w := a :: (append v w)
|
||||
definition append : Π {n m : nat}, vector A n → vector A m → vector A (n ⊕ m)
|
||||
| @append 0 m nil w := w
|
||||
| @append (succ n) m (a::v) w := a :: (append v w)
|
||||
|
||||
theorem append_nil {n : nat} (v : vector A n) : append nil v = v :=
|
||||
rfl
|
||||
|
|
@ -94,9 +94,9 @@ namespace vector
|
|||
append (h::t) v = h :: (append t v) :=
|
||||
rfl
|
||||
|
||||
definition unzip : Π {n : nat}, vector (A × B) n → vector A n × vector B n,
|
||||
unzip nil := (nil, nil),
|
||||
unzip ((a, b) :: v) := (a :: pr₁ (unzip v), b :: pr₂ (unzip v))
|
||||
definition unzip : Π {n : nat}, vector (A × B) n → vector A n × vector B n
|
||||
| unzip nil := (nil, nil)
|
||||
| unzip ((a, b) :: v) := (a :: pr₁ (unzip v), b :: pr₂ (unzip v))
|
||||
|
||||
theorem unzip_nil : unzip (@nil (A × B)) = (nil, nil) :=
|
||||
rfl
|
||||
|
|
@ -105,9 +105,9 @@ namespace vector
|
|||
unzip ((a, b) :: v) = (a :: pr₁ (unzip v), b :: pr₂ (unzip v)) :=
|
||||
rfl
|
||||
|
||||
definition zip : Π {n : nat}, vector A n → vector B n → vector (A × B) n,
|
||||
zip nil nil := nil,
|
||||
zip (a::va) (b::vb) := ((a, b) :: zip va vb)
|
||||
definition zip : Π {n : nat}, vector A n → vector B n → vector (A × B) n
|
||||
| zip nil nil := nil
|
||||
| zip (a::va) (b::vb) := ((a, b) :: zip va vb)
|
||||
|
||||
theorem zip_nil_nil : zip (@nil A) (@nil B) = nil :=
|
||||
rfl
|
||||
|
|
@ -116,26 +116,26 @@ namespace vector
|
|||
zip (a::va) (b::vb) = ((a, b) :: zip va vb) :=
|
||||
rfl
|
||||
|
||||
theorem unzip_zip : ∀ {n : nat} (v₁ : vector A n) (v₂ : vector B n), unzip (zip v₁ v₂) = (v₁, v₂),
|
||||
@unzip_zip 0 nil nil := rfl,
|
||||
@unzip_zip (succ n) (a::va) (b::vb) := calc
|
||||
theorem unzip_zip : ∀ {n : nat} (v₁ : vector A n) (v₂ : vector B n), unzip (zip v₁ v₂) = (v₁, v₂)
|
||||
| @unzip_zip 0 nil nil := rfl
|
||||
| @unzip_zip (succ n) (a::va) (b::vb) := calc
|
||||
unzip (zip (a :: va) (b :: vb))
|
||||
= (a :: pr₁ (unzip (zip va vb)), b :: pr₂ (unzip (zip va vb))) : rfl
|
||||
... = (a :: pr₁ (va, vb), b :: pr₂ (va, vb)) : {unzip_zip va vb}
|
||||
... = (a :: va, b :: vb) : rfl
|
||||
|
||||
theorem zip_unzip : ∀ {n : nat} (v : vector (A × B) n), zip (pr₁ (unzip v)) (pr₂ (unzip v)) = v,
|
||||
@zip_unzip 0 nil := rfl,
|
||||
@zip_unzip (succ n) ((a, b) :: v) := calc
|
||||
theorem zip_unzip : ∀ {n : nat} (v : vector (A × B) n), zip (pr₁ (unzip v)) (pr₂ (unzip v)) = v
|
||||
| @zip_unzip 0 nil := rfl
|
||||
| @zip_unzip (succ n) ((a, b) :: v) := calc
|
||||
zip (pr₁ (unzip ((a, b) :: v))) (pr₂ (unzip ((a, b) :: v)))
|
||||
= (a, b) :: zip (pr₁ (unzip v)) (pr₂ (unzip v)) : rfl
|
||||
... = (a, b) :: v : {zip_unzip v}
|
||||
|
||||
/- Concat -/
|
||||
|
||||
definition concat : Π {n : nat}, vector A n → A → vector A (succ n),
|
||||
concat nil a := a :: nil,
|
||||
concat (b::v) a := b :: concat v a
|
||||
definition concat : Π {n : nat}, vector A n → A → vector A (succ n)
|
||||
| concat nil a := a :: nil
|
||||
| concat (b::v) a := b :: concat v a
|
||||
|
||||
theorem concat_nil (a : A) : concat nil a = a :: nil :=
|
||||
rfl
|
||||
|
|
@ -143,9 +143,9 @@ namespace vector
|
|||
theorem concat_cons {n : nat} (b : A) (v : vector A n) (a : A) : concat (b :: v) a = b :: concat v a :=
|
||||
rfl
|
||||
|
||||
theorem last_concat : ∀ {n : nat} (v : vector A n) (a : A), last (concat v a) = a,
|
||||
@last_concat 0 nil a := rfl,
|
||||
@last_concat (succ n) (b::v) a := calc
|
||||
theorem last_concat : ∀ {n : nat} (v : vector A n) (a : A), last (concat v a) = a
|
||||
| @last_concat 0 nil a := rfl
|
||||
| @last_concat (succ n) (b::v) a := calc
|
||||
last (concat (b::v) a) = last (concat v a) : rfl
|
||||
... = a : last_concat v a
|
||||
end vector
|
||||
|
|
|
|||
|
|
@ -29,14 +29,14 @@ namespace nat
|
|||
protected definition is_inhabited [instance] : inhabited nat :=
|
||||
inhabited.mk zero
|
||||
|
||||
protected definition has_decidable_eq [instance] : ∀ x y : nat, decidable (x = y),
|
||||
has_decidable_eq zero zero := inl rfl,
|
||||
has_decidable_eq (succ x) zero := inr (λ h, nat.no_confusion h),
|
||||
has_decidable_eq zero (succ y) := inr (λ h, nat.no_confusion h),
|
||||
has_decidable_eq (succ x) (succ y) :=
|
||||
if H : x = y
|
||||
then inl (eq.rec_on H rfl)
|
||||
else inr (λ h : succ x = succ y, nat.no_confusion h (λ heq : x = y, absurd heq H))
|
||||
protected definition has_decidable_eq [instance] : ∀ x y : nat, decidable (x = y)
|
||||
| has_decidable_eq zero zero := inl rfl
|
||||
| has_decidable_eq (succ x) zero := inr (λ h, nat.no_confusion h)
|
||||
| has_decidable_eq zero (succ y) := inr (λ h, nat.no_confusion h)
|
||||
| has_decidable_eq (succ x) (succ y) :=
|
||||
if H : x = y
|
||||
then inl (eq.rec_on H rfl)
|
||||
else inr (λ h : succ x = succ y, nat.no_confusion h (λ heq : x = y, absurd heq H))
|
||||
|
||||
-- less-than is well-founded
|
||||
definition lt.wf [instance] : well_founded lt :=
|
||||
|
|
|
|||
|
|
@ -94,7 +94,7 @@ notation `reverts` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)`
|
|||
opaque definition assert_hypothesis (id : expr) (e : expr) : tactic := builtin
|
||||
|
||||
infixl `;`:15 := and_then
|
||||
notation `[` h:10 `|`:10 r:(foldl:10 `|` (e r, or_else r e) h) `]` := r
|
||||
notation `[` h `|` r:(foldl `|` (e r, or_else r e) h) `]` := r
|
||||
|
||||
definition try (t : tactic) : tactic := [t | id]
|
||||
definition repeat1 (t : tactic) : tactic := t ; repeat t
|
||||
|
|
|
|||
|
|
@ -440,8 +440,8 @@ static void erase_local_binder_info(buffer<expr> & ps) {
|
|||
p = update_local(p, binder_info());
|
||||
}
|
||||
|
||||
static bool is_curr_with_or_comma(parser & p) {
|
||||
return p.curr_is_token(get_with_tk()) || p.curr_is_token(get_comma_tk());
|
||||
static bool is_curr_with_or_comma_or_bar(parser & p) {
|
||||
return p.curr_is_token(get_with_tk()) || p.curr_is_token(get_comma_tk()) || p.curr_is_token(get_bar_tk());
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
@ -515,6 +515,16 @@ static void throw_invalid_equation_lhs(name const & n, pos_info const & p) {
|
|||
<< n << "' in the left-hand-side does not correspond to function(s) being defined", p);
|
||||
}
|
||||
|
||||
static bool is_eqn_prefix(parser & p) {
|
||||
return p.curr_is_token(get_bar_tk()) || p.curr_is_token(get_comma_tk());
|
||||
}
|
||||
|
||||
static void check_eqn_prefix(parser & p) {
|
||||
if (!is_eqn_prefix(p))
|
||||
throw parser_error("invalid declaration, ',' or '|' expected", p.pos());
|
||||
p.next();
|
||||
}
|
||||
|
||||
expr parse_equations(parser & p, name const & n, expr const & type, buffer<name> & auxs,
|
||||
optional<local_environment> const & lenv, buffer<expr> const & ps,
|
||||
pos_info const & def_pos) {
|
||||
|
|
@ -524,7 +534,7 @@ expr parse_equations(parser & p, name const & n, expr const & type, buffer<name>
|
|||
parser::local_scope scope1(p, lenv);
|
||||
for (expr const & param : ps)
|
||||
p.add_local(param);
|
||||
lean_assert(is_curr_with_or_comma(p));
|
||||
lean_assert(is_curr_with_or_comma_or_bar(p));
|
||||
fns.push_back(mk_local(n, type));
|
||||
if (p.curr_is_token(get_with_tk())) {
|
||||
while (p.curr_is_token(get_with_tk())) {
|
||||
|
|
@ -538,7 +548,7 @@ expr parse_equations(parser & p, name const & n, expr const & type, buffer<name>
|
|||
fns.push_back(g);
|
||||
}
|
||||
}
|
||||
p.check_token_next(get_comma_tk(), "invalid declaration, ',' expected");
|
||||
check_eqn_prefix(p);
|
||||
for (expr const & fn : fns)
|
||||
p.add_local(fn);
|
||||
while (true) {
|
||||
|
|
@ -574,7 +584,7 @@ expr parse_equations(parser & p, name const & n, expr const & type, buffer<name>
|
|||
expr rhs = p.parse_expr();
|
||||
eqns.push_back(Fun(fns, Fun(locals, p.save_pos(mk_equation(lhs, rhs), assign_pos), p)));
|
||||
}
|
||||
if (!p.curr_is_token(get_comma_tk()))
|
||||
if (!is_eqn_prefix(p))
|
||||
break;
|
||||
p.next();
|
||||
}
|
||||
|
|
@ -594,6 +604,8 @@ expr parse_equations(parser & p, name const & n, expr const & type, buffer<name>
|
|||
expr parse_match(parser & p, unsigned, expr const *, pos_info const & pos) {
|
||||
expr t = p.parse_expr();
|
||||
p.check_token_next(get_with_tk(), "invalid 'match' expression, 'with' expected");
|
||||
if (is_eqn_prefix(p))
|
||||
p.next();
|
||||
buffer<expr> eqns;
|
||||
expr fn = mk_local(p.mk_fresh_name(), "match", mk_expr_placeholder(), binder_info());
|
||||
while (true) {
|
||||
|
|
@ -621,7 +633,7 @@ expr parse_match(parser & p, unsigned, expr const *, pos_info const & pos) {
|
|||
expr rhs = p.parse_expr();
|
||||
eqns.push_back(Fun(fn, Fun(locals, p.save_pos(mk_equation(lhs, rhs), assign_pos), p)));
|
||||
}
|
||||
if (!p.curr_is_token(get_comma_tk()))
|
||||
if (!is_eqn_prefix(p))
|
||||
break;
|
||||
p.next();
|
||||
}
|
||||
|
|
@ -685,7 +697,7 @@ class definition_cmd_fn {
|
|||
m_p.next();
|
||||
auto pos = m_p.pos();
|
||||
m_type = m_p.parse_expr();
|
||||
if (is_curr_with_or_comma(m_p)) {
|
||||
if (is_curr_with_or_comma_or_bar(m_p)) {
|
||||
m_value = parse_equations(m_p, m_name, m_type, m_aux_decls,
|
||||
optional<local_environment>(), buffer<expr>(), m_pos);
|
||||
} else if (!is_definition() && !m_p.curr_is_token(get_assign_tk())) {
|
||||
|
|
@ -704,7 +716,7 @@ class definition_cmd_fn {
|
|||
if (m_p.curr_is_token(get_colon_tk())) {
|
||||
m_p.next();
|
||||
m_type = m_p.parse_scoped_expr(ps, *lenv);
|
||||
if (is_curr_with_or_comma(m_p)) {
|
||||
if (is_curr_with_or_comma_or_bar(m_p)) {
|
||||
m_value = parse_equations(m_p, m_name, m_type, m_aux_decls, lenv, ps, m_pos);
|
||||
} else if (!is_definition() && !m_p.curr_is_token(get_assign_tk())) {
|
||||
check_end_of_theorem(m_p);
|
||||
|
|
|
|||
|
|
@ -1,15 +1,15 @@
|
|||
open nat
|
||||
|
||||
definition foo : nat → nat,
|
||||
foo (0 + x) := x
|
||||
definition foo : nat → nat
|
||||
| foo (0 + x) := x
|
||||
|
||||
definition foo : nat → nat → nat,
|
||||
foo 0 _ := 0,
|
||||
foo x ⌞y⌟ := x
|
||||
definition foo : nat → nat → nat
|
||||
| foo 0 _ := 0
|
||||
| foo x ⌞y⌟ := x
|
||||
|
||||
definition foo : nat → nat → nat,
|
||||
foo 0 _ := 0,
|
||||
foo ⌞x⌟ x := x
|
||||
definition foo : nat → nat → nat
|
||||
| foo 0 _ := 0
|
||||
| foo ⌞x⌟ x := x
|
||||
|
||||
inductive tree (A : Type) :=
|
||||
node : tree_list A → tree A,
|
||||
|
|
@ -19,18 +19,18 @@ nil {} : tree_list A,
|
|||
cons : tree A → tree_list A → tree_list A
|
||||
|
||||
definition is_leaf {A : Type} : tree A → bool
|
||||
with is_leaf_aux : tree_list A → bool,
|
||||
is_leaf (tree.node _) := bool.ff,
|
||||
is_leaf (tree.leaf _) := bool.tt,
|
||||
is_leaf_aux tree_list.nil := bool.ff,
|
||||
is_leaf_aux (tree_list.cons _ _) := bool.ff
|
||||
with is_leaf_aux : tree_list A → bool
|
||||
| is_leaf (tree.node _) := bool.ff
|
||||
| is_leaf (tree.leaf _) := bool.tt
|
||||
| is_leaf_aux tree_list.nil := bool.ff
|
||||
| is_leaf_aux (tree_list.cons _ _) := bool.ff
|
||||
|
||||
definition foo : nat → nat,
|
||||
foo 0 := 0,
|
||||
foo (x+1) := let y := x + 2 in y * y
|
||||
definition foo : nat → nat
|
||||
| foo 0 := 0
|
||||
| foo (x+1) := let y := x + 2 in y * y
|
||||
|
||||
example : foo 5 = 36 := rfl
|
||||
|
||||
definition boo : nat → nat,
|
||||
boo (x + 1) := boo (x + 2),
|
||||
boo 0 := 0
|
||||
definition boo : nat → nat
|
||||
| boo (x + 1) := boo (x + 2)
|
||||
| boo 0 := 0
|
||||
|
|
|
|||
|
|
@ -1,8 +1,8 @@
|
|||
bad_eqns.lean:4:0: error: invalid argument, it is not a constructor, variable, nor it is marked as an inaccessible pattern
|
||||
bad_eqns.lean:4:2: error: invalid argument, it is not a constructor, variable, nor it is marked as an inaccessible pattern
|
||||
0 + x
|
||||
in the following equation left-hand-side
|
||||
foo (0 + x)
|
||||
bad_eqns.lean:8:0: error: invalid equation left-hand-side, variable 'y' only occurs in inaccessible terms in the following equation left-hand-side
|
||||
bad_eqns.lean:8:2: error: invalid equation left-hand-side, variable 'y' only occurs in inaccessible terms in the following equation left-hand-side
|
||||
foo x y
|
||||
bad_eqns.lean:10:11: error: invalid recursive equations for 'foo', inconsistent use of inaccessible term annotation, in some equations a pattern is a constructor, and in another it is an inaccessible term
|
||||
bad_eqns.lean:21:11: error: mutual recursion is not needed when defining non-recursive functions
|
||||
|
|
|
|||
|
|
@ -2,13 +2,13 @@ open eq eq.ops
|
|||
|
||||
variable {A : Type}
|
||||
|
||||
definition trans : Π {x y z : A} (p : x = y) (q : y = z), x = z,
|
||||
trans (refl a) (refl a) := refl a
|
||||
definition trans : Π {x y z : A} (p : x = y) (q : y = z), x = z
|
||||
| trans (refl a) (refl a) := refl a
|
||||
|
||||
set_option pp.purify_locals false
|
||||
|
||||
definition con_inv_cancel_left : Π {x y z : A} (p : x = y) (q : x = z), p ⬝ (p⁻¹ ⬝ q) = q,
|
||||
con_inv_cancel_left (refl a) (refl a) := refl (refl a)
|
||||
definition con_inv_cancel_left : Π {x y z : A} (p : x = y) (q : x = z), p ⬝ (p⁻¹ ⬝ q) = q
|
||||
| con_inv_cancel_left (refl a) (refl a) := refl (refl a)
|
||||
|
||||
definition inv_con_cancel_left : Π {x y z : A} (p : x = y) (q : y = z), p⁻¹ ⬝ (p ⬝ q) = q,
|
||||
inv_con_cancel_left (refl a) (refl a) := refl (refl a)
|
||||
definition inv_con_cancel_left : Π {x y z : A} (p : x = y) (q : y = z), p⁻¹ ⬝ (p ⬝ q) = q
|
||||
| inv_con_cancel_left (refl a) (refl a) := refl (refl a)
|
||||
|
|
|
|||
|
|
@ -6,8 +6,8 @@ cons : Π {n}, A → vector A n → vector A (succ n)
|
|||
|
||||
infixr `::` := vector.cons
|
||||
|
||||
definition swap {A : Type} : Π {n}, vector A (succ (succ n)) → vector A (succ (succ n)),
|
||||
swap (a :: b :: vs) := b :: a :: vs
|
||||
definition swap {A : Type} : Π {n}, vector A (succ (succ n)) → vector A (succ (succ n))
|
||||
| swap (a :: b :: vs) := b :: a :: vs
|
||||
|
||||
-- Remark: in the current approach for HoTT, the equation
|
||||
-- swap (a :: b :: v) = b :: a :: v
|
||||
|
|
|
|||
|
|
@ -3,12 +3,12 @@ open nat vector
|
|||
|
||||
variable {A : Type}
|
||||
|
||||
definition foo : Π {n : nat}, vector A n → nat,
|
||||
foo nil := 0,
|
||||
foo (a :: b :: v) := 0
|
||||
definition foo : Π {n : nat}, vector A n → nat
|
||||
| foo nil := 0
|
||||
| foo (a :: b :: v) := 0
|
||||
|
||||
set_option pp.implicit false
|
||||
|
||||
definition foo : Π {n : nat}, vector A n → nat,
|
||||
foo nil := 0,
|
||||
foo (a :: b :: v) := 0
|
||||
definition foo : Π {n : nat}, vector A n → nat
|
||||
| foo nil := 0
|
||||
| foo (a :: b :: v) := 0
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
open nat
|
||||
|
||||
definition foo : nat → nat,
|
||||
foo zero := _,
|
||||
foo (succ a) := _
|
||||
definition foo : nat → nat
|
||||
| foo zero := _
|
||||
| foo (succ a) := _
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
place_eqn.lean:4:16: error: don't know how to synthesize placeholder
|
||||
place_eqn.lean:4:18: error: don't know how to synthesize placeholder
|
||||
foo : ℕ → ℕ
|
||||
⊢ ℕ
|
||||
place_eqn.lean:5:16: error: don't know how to synthesize placeholder
|
||||
place_eqn.lean:5:18: error: don't know how to synthesize placeholder
|
||||
foo : ℕ → ℕ,
|
||||
a : ℕ
|
||||
⊢ ℕ
|
||||
|
|
|
|||
|
|
@ -3,12 +3,12 @@ open nat eq.ops
|
|||
|
||||
theorem lcm_dvd {m n k : nat} (H1 : (m | k)) (H2 : (n | k)) : (lcm m n | k) :=
|
||||
match eq_zero_or_pos k with
|
||||
@or.inl _ _ kzero :=
|
||||
| @or.inl _ _ kzero :=
|
||||
begin
|
||||
rewrite kzero,
|
||||
apply dvd_zero
|
||||
end,
|
||||
@or.inr _ _ kpos :=
|
||||
end
|
||||
| @or.inr _ _ kpos :=
|
||||
obtain (p : nat) (km : k = m * p), from exists_eq_mul_right_of_dvd H1,
|
||||
obtain (q : nat) (kn : k = n * q), from exists_eq_mul_right_of_dvd H2,
|
||||
begin
|
||||
|
|
|
|||
|
|
@ -3,14 +3,14 @@ monday, tuesday, wednesday, thursday, friday, saturday, sunday
|
|||
|
||||
open day
|
||||
|
||||
definition next_weekday : day → day,
|
||||
next_weekday monday := tuesday,
|
||||
next_weekday tuesday := wednesday,
|
||||
next_weekday wednesday := thursday,
|
||||
next_weekday thursday := friday,
|
||||
next_weekday friday := monday,
|
||||
next_weekday saturday := monday,
|
||||
next_weekday sunday := monday
|
||||
definition next_weekday : day → day
|
||||
| next_weekday monday := tuesday
|
||||
| next_weekday tuesday := wednesday
|
||||
| next_weekday wednesday := thursday
|
||||
| next_weekday thursday := friday
|
||||
| next_weekday friday := monday
|
||||
| next_weekday saturday := monday
|
||||
| next_weekday sunday := monday
|
||||
|
||||
example : next_weekday (next_weekday monday) = wednesday :=
|
||||
rfl
|
||||
|
|
|
|||
|
|
@ -9,13 +9,13 @@ allf : (nat → formula) → formula
|
|||
namespace formula
|
||||
definition implies (a b : Prop) : Prop := a → b
|
||||
|
||||
definition denote : formula → Prop,
|
||||
denote (eqf n1 n2) := n1 = n2,
|
||||
denote (andf f1 f2) := denote f1 ∧ denote f2,
|
||||
denote (impf f1 f2) := implies (denote f1) (denote f2),
|
||||
denote (orf f1 f2) := denote f1 ∨ denote f2,
|
||||
denote (notf f) := ¬ denote f,
|
||||
denote (allf f) := ∀ n : nat, denote (f n)
|
||||
definition denote : formula → Prop
|
||||
| denote (eqf n1 n2) := n1 = n2
|
||||
| denote (andf f1 f2) := denote f1 ∧ denote f2
|
||||
| denote (impf f1 f2) := implies (denote f1) (denote f2)
|
||||
| denote (orf f1 f2) := denote f1 ∨ denote f2
|
||||
| denote (notf f) := ¬ denote f
|
||||
| denote (allf f) := ∀ n : nat, denote (f n)
|
||||
|
||||
theorem denote_eqf (n1 n2 : nat) : denote (eqf n1 n2) = (n1 = n2) :=
|
||||
rfl
|
||||
|
|
|
|||
|
|
@ -3,12 +3,12 @@ monday, tuesday, wednesday, thursday, friday, saturday, sunday
|
|||
|
||||
open day
|
||||
|
||||
definition next_weekday : day → day,
|
||||
next_weekday monday := tuesday,
|
||||
next_weekday tuesday := wednesday,
|
||||
next_weekday wednesday := thursday,
|
||||
next_weekday thursday := friday,
|
||||
next_weekday _ := monday
|
||||
definition next_weekday : day → day
|
||||
| next_weekday monday := tuesday
|
||||
| next_weekday tuesday := wednesday
|
||||
| next_weekday wednesday := thursday
|
||||
| next_weekday thursday := friday
|
||||
| next_weekday _ := monday
|
||||
|
||||
theorem next_weekday_monday : next_weekday monday = tuesday := rfl
|
||||
theorem next_weekday_tuesday : next_weekday tuesday = wednesday := rfl
|
||||
|
|
|
|||
|
|
@ -1,10 +1,10 @@
|
|||
open nat bool inhabited
|
||||
|
||||
definition diag : bool → bool → bool → nat,
|
||||
diag _ tt ff := 1,
|
||||
diag ff _ tt := 2,
|
||||
diag tt ff _ := 3,
|
||||
diag _ _ _ := arbitrary nat
|
||||
definition diag : bool → bool → bool → nat
|
||||
| diag _ tt ff := 1
|
||||
| diag ff _ tt := 2
|
||||
| diag tt ff _ := 3
|
||||
| diag _ _ _ := arbitrary nat
|
||||
|
||||
theorem diag1 (a : bool) : diag a tt ff = 1 :=
|
||||
bool.cases_on a rfl rfl
|
||||
|
|
|
|||
|
|
@ -1,13 +1,13 @@
|
|||
open nat
|
||||
|
||||
definition f : nat → nat → nat,
|
||||
f _ 0 := 0,
|
||||
f 0 _ := 1,
|
||||
f _ _ := arbitrary nat
|
||||
definition f : nat → nat → nat
|
||||
| f _ 0 := 0
|
||||
| f 0 _ := 1
|
||||
| f _ _ := arbitrary nat
|
||||
|
||||
theorem f_zero_right : ∀ a, f a 0 = 0,
|
||||
f_zero_right 0 := rfl,
|
||||
f_zero_right (succ _) := rfl
|
||||
theorem f_zero_right : ∀ a, f a 0 = 0
|
||||
| f_zero_right 0 := rfl
|
||||
| f_zero_right (succ _) := rfl
|
||||
|
||||
theorem f_zero_succ (a : nat) : f 0 (a+1) = 1 :=
|
||||
rfl
|
||||
|
|
|
|||
|
|
@ -1,13 +1,13 @@
|
|||
open nat decidable
|
||||
|
||||
definition has_decidable_eq : ∀ a b : nat, decidable (a = b),
|
||||
has_decidable_eq 0 0 := inl rfl,
|
||||
has_decidable_eq (a+1) 0 := inr (λ h, nat.no_confusion h),
|
||||
has_decidable_eq 0 (b+1) := inr (λ h, nat.no_confusion h),
|
||||
has_decidable_eq (a+1) (b+1) :=
|
||||
if H : a = b
|
||||
then inl (eq.rec_on H rfl)
|
||||
else inr (λ h : a+1 = b+1, nat.no_confusion h (λ e : a = b, absurd e H))
|
||||
definition has_decidable_eq : ∀ a b : nat, decidable (a = b)
|
||||
| has_decidable_eq 0 0 := inl rfl
|
||||
| has_decidable_eq (a+1) 0 := inr (λ h, nat.no_confusion h)
|
||||
| has_decidable_eq 0 (b+1) := inr (λ h, nat.no_confusion h)
|
||||
| has_decidable_eq (a+1) (b+1) :=
|
||||
if H : a = b
|
||||
then inl (eq.rec_on H rfl)
|
||||
else inr (λ h : a+1 = b+1, nat.no_confusion h (λ e : a = b, absurd e H))
|
||||
|
||||
check has_decidable_eq
|
||||
print definition has_decidable_eq
|
||||
|
|
|
|||
|
|
@ -3,9 +3,9 @@ open list
|
|||
|
||||
set_option pp.implicit true
|
||||
|
||||
definition append : Π {A : Type}, list A → list A → list A,
|
||||
append nil l := l,
|
||||
append (h :: t) l := h :: (append t l)
|
||||
definition append : Π {A : Type}, list A → list A → list A
|
||||
| append nil l := l
|
||||
| append (h :: t) l := h :: (append t l)
|
||||
|
||||
theorem append_nil {A : Type} (l : list A) : append nil l = l :=
|
||||
rfl
|
||||
|
|
|
|||
|
|
@ -4,9 +4,9 @@ open list
|
|||
variable {A : Type}
|
||||
set_option pp.implicit true
|
||||
|
||||
definition append : list A → list A → list A,
|
||||
append nil l := l,
|
||||
append (h :: t) l := h :: (append t l)
|
||||
definition append : list A → list A → list A
|
||||
| append nil l := l
|
||||
| append (h :: t) l := h :: (append t l)
|
||||
|
||||
theorem append_nil (l : list A) : append nil l = l :=
|
||||
rfl
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
open nat
|
||||
|
||||
definition lt_of_succ : ∀ {a b : nat}, succ a < b → a < b,
|
||||
lt_of_succ (lt.base (succ a)) := lt.trans (lt.base a) (lt.base (succ a)),
|
||||
lt_of_succ (lt.step h) := lt.step (lt_of_succ h)
|
||||
definition lt_of_succ : ∀ {a b : nat}, succ a < b → a < b
|
||||
| lt_of_succ (lt.base (succ a)) := lt.trans (lt.base a) (lt.base (succ a))
|
||||
| lt_of_succ (lt.step h) := lt.step (lt_of_succ h)
|
||||
|
|
|
|||
|
|
@ -1,9 +1,9 @@
|
|||
import data.vector
|
||||
open nat vector
|
||||
|
||||
definition last {A : Type} : Π {n}, vector A (succ n) → A,
|
||||
last (a :: nil) := a,
|
||||
last (a :: v) := last v
|
||||
definition last {A : Type} : Π {n}, vector A (succ n) → A
|
||||
| last (a :: nil) := a
|
||||
| last (a :: v) := last v
|
||||
|
||||
theorem last_cons_nil {A : Type} {n : nat} (a : A) : last (a :: nil) = a :=
|
||||
rfl
|
||||
|
|
|
|||
|
|
@ -3,9 +3,9 @@ open nat vector prod
|
|||
|
||||
variables {A B : Type}
|
||||
|
||||
definition unzip : Π {n}, vector (A × B) n → vector A n × vector B n,
|
||||
unzip nil := (nil, nil),
|
||||
unzip ((a, b) :: t) := (a :: pr₁ (unzip t), b :: pr₂ (unzip t))
|
||||
definition unzip : Π {n}, vector (A × B) n → vector A n × vector B n
|
||||
| unzip nil := (nil, nil)
|
||||
| unzip ((a, b) :: t) := (a :: pr₁ (unzip t), b :: pr₂ (unzip t))
|
||||
|
||||
theorem unzip_nil : unzip nil = (@nil A, @nil B) :=
|
||||
rfl
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
definition symm {A : Type} : Π {a b : A}, a = b → b = a,
|
||||
symm rfl := rfl
|
||||
definition symm {A : Type} : Π {a b : A}, a = b → b = a
|
||||
| symm rfl := rfl
|
||||
|
||||
definition trans {A : Type} : Π {a b c : A}, a = b → b = c → a = c,
|
||||
trans rfl rfl := rfl
|
||||
definition trans {A : Type} : Π {a b c : A}, a = b → b = c → a = c
|
||||
| trans rfl rfl := rfl
|
||||
|
|
|
|||
|
|
@ -7,9 +7,9 @@ context
|
|||
parameter [H : decidable_pred p]
|
||||
include H
|
||||
|
||||
definition filter : list A → list A,
|
||||
filter nil := nil,
|
||||
filter (a :: l) := if p a then a :: filter l else filter l
|
||||
definition filter : list A → list A
|
||||
| filter nil := nil
|
||||
| filter (a :: l) := if p a then a :: filter l else filter l
|
||||
|
||||
theorem filter_nil : filter nil = nil :=
|
||||
rfl
|
||||
|
|
|
|||
|
|
@ -3,9 +3,9 @@ eqf : nat → nat → formula,
|
|||
impf : formula → formula → formula
|
||||
|
||||
namespace formula
|
||||
definition denote : formula → Prop,
|
||||
denote (eqf n1 n2) := n1 = n2,
|
||||
denote (impf f1 f2) := denote f1 → denote f2
|
||||
definition denote : formula → Prop
|
||||
| denote (eqf n1 n2) := n1 = n2
|
||||
| denote (impf f1 f2) := denote f1 → denote f2
|
||||
|
||||
theorem denote_eqf (n1 n2 : nat) : denote (eqf n1 n2) = (n1 = n2) :=
|
||||
rfl
|
||||
|
|
|
|||
|
|
@ -1,9 +1,9 @@
|
|||
import data.list
|
||||
open list
|
||||
|
||||
definition head {A : Type} : Π (l : list A), l ≠ nil → A,
|
||||
head nil h := absurd rfl h,
|
||||
head (a :: l) _ := a
|
||||
definition head {A : Type} : Π (l : list A), l ≠ nil → A
|
||||
| head nil h := absurd rfl h
|
||||
| head (a :: l) _ := a
|
||||
|
||||
theorem head_cons {A : Type} (a : A) (l : list A) (h : a :: l ≠ nil) : head (a :: l) h = a :=
|
||||
rfl
|
||||
|
|
|
|||
|
|
@ -9,9 +9,9 @@ cons : tree A → tree_list A → tree_list A
|
|||
|
||||
namespace tree_list
|
||||
|
||||
definition len {A : Type} : tree_list A → nat,
|
||||
len (nil A) := 0,
|
||||
len (cons t l) := len l + 1
|
||||
definition len {A : Type} : tree_list A → nat
|
||||
| len (nil A) := 0
|
||||
| len (cons t l) := len l + 1
|
||||
|
||||
theorem len_nil {A : Type} : len (nil A) = 0 :=
|
||||
rfl
|
||||
|
|
|
|||
|
|
@ -11,11 +11,11 @@ namespace tree
|
|||
open tree_list
|
||||
|
||||
definition size {A : Type} : tree A → nat
|
||||
with size_l : tree_list A → nat,
|
||||
size (leaf a) := 1,
|
||||
size (node l) := size_l l,
|
||||
size_l !nil := 0,
|
||||
size_l (cons t l) := size t + size_l l
|
||||
with size_l : tree_list A → nat
|
||||
| size (leaf a) := 1
|
||||
| size (node l) := size_l l
|
||||
| size_l !nil := 0
|
||||
| size_l (cons t l) := size t + size_l l
|
||||
|
||||
variables {A : Type}
|
||||
|
||||
|
|
@ -32,13 +32,13 @@ theorem size_l_cons (t : tree A) (l : tree_list A) : size_l (cons t l) = size t
|
|||
rfl
|
||||
|
||||
definition eq_tree {A : Type} : tree A → tree A → Prop
|
||||
with eq_tree_list : tree_list A → tree_list A → Prop,
|
||||
eq_tree (leaf a₁) (leaf a₂) := a₁ = a₂,
|
||||
eq_tree (node l₁) (node l₂) := eq_tree_list l₁ l₂,
|
||||
eq_tree _ _ := false,
|
||||
eq_tree_list !nil !nil := true,
|
||||
eq_tree_list (cons t₁ l₁) (cons t₂ l₂) := eq_tree t₁ t₂ ∧ eq_tree_list l₁ l₂,
|
||||
eq_tree_list _ _ := false
|
||||
with eq_tree_list : tree_list A → tree_list A → Prop
|
||||
| eq_tree (leaf a₁) (leaf a₂) := a₁ = a₂
|
||||
| eq_tree (node l₁) (node l₂) := eq_tree_list l₁ l₂
|
||||
| eq_tree _ _ := false
|
||||
| eq_tree_list !nil !nil := true
|
||||
| eq_tree_list (cons t₁ l₁) (cons t₂ l₂) := eq_tree t₁ t₂ ∧ eq_tree_list l₁ l₂
|
||||
| eq_tree_list _ _ := false
|
||||
|
||||
theorem eq_tree_leaf (a₁ a₂ : A) : eq_tree (leaf a₁) (leaf a₂) = (a₁ = a₂) :=
|
||||
rfl
|
||||
|
|
|
|||
|
|
@ -6,6 +6,6 @@ definition Nat := N
|
|||
|
||||
open N
|
||||
|
||||
definition add : Nat → Nat → Nat,
|
||||
add O b := b,
|
||||
add (S a) b := S (add a b)
|
||||
definition add : Nat → Nat → Nat
|
||||
| add O b := b
|
||||
| add (S a) b := S (add a b)
|
||||
|
|
|
|||
|
|
@ -1,8 +1,8 @@
|
|||
import data.vector
|
||||
open nat vector
|
||||
|
||||
definition swap {A : Type} : Π {n}, vector A (succ (succ n)) → vector A (succ (succ n)),
|
||||
swap (a :: b :: vs) := b :: a :: vs
|
||||
definition swap {A : Type} : Π {n}, vector A (succ (succ n)) → vector A (succ (succ n))
|
||||
| swap (a :: b :: vs) := b :: a :: vs
|
||||
|
||||
example (n : nat) (a b : num) (v : vector num n) : swap (a :: b :: v) = b :: a :: v :=
|
||||
rfl
|
||||
|
|
|
|||
|
|
@ -1,9 +1,9 @@
|
|||
open nat
|
||||
|
||||
definition half : nat → nat,
|
||||
half 0 := 0,
|
||||
half 1 := 0,
|
||||
half (x+2) := half x + 1
|
||||
definition half : nat → nat
|
||||
| half 0 := 0
|
||||
| half 1 := 0
|
||||
| half (x+2) := half x + 1
|
||||
|
||||
theorem half0 : half 0 = 0 :=
|
||||
rfl
|
||||
|
|
|
|||
|
|
@ -1,9 +1,9 @@
|
|||
open nat
|
||||
|
||||
definition fib : nat → nat,
|
||||
fib 0 := 1,
|
||||
fib 1 := 1,
|
||||
fib (x+2) := fib x + fib (x+1)
|
||||
definition fib : nat → nat
|
||||
| fib 0 := 1
|
||||
| fib 1 := 1
|
||||
| fib (x+2) := fib x + fib (x+1)
|
||||
|
||||
theorem fib0 : fib 0 = 1 :=
|
||||
rfl
|
||||
|
|
|
|||
|
|
@ -1,9 +1,9 @@
|
|||
import data.list
|
||||
open list
|
||||
|
||||
definition append {A : Type} : list A → list A → list A,
|
||||
append nil l := l,
|
||||
append (h :: t) l := h :: (append t l)
|
||||
definition append {A : Type} : list A → list A → list A
|
||||
| append nil l := l
|
||||
| append (h :: t) l := h :: (append t l)
|
||||
|
||||
theorem append_nil {A : Type} (l : list A) : append nil l = l :=
|
||||
rfl
|
||||
|
|
|
|||
|
|
@ -1,9 +1,9 @@
|
|||
import data.vector
|
||||
open nat vector
|
||||
|
||||
definition diag {A : Type} : Π {n}, vector (vector A n) n → vector A n,
|
||||
diag nil := nil,
|
||||
diag ((a :: va) :: vs) := a :: diag (map tail vs)
|
||||
definition diag {A : Type} : Π {n}, vector (vector A n) n → vector A n
|
||||
| diag nil := nil
|
||||
| diag ((a :: va) :: vs) := a :: diag (map tail vs)
|
||||
|
||||
theorem diag_nil (A : Type) : diag (@nil (vector A 0)) = nil :=
|
||||
rfl
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
import data.vector
|
||||
open vector
|
||||
|
||||
definition map {A B C : Type} (f : A → B → C) : Π {n}, vector A n → vector B n → vector C n,
|
||||
map nil nil := nil,
|
||||
map (a :: va) (b :: vb) := f a b :: map va vb
|
||||
definition map {A B C : Type} (f : A → B → C) : Π {n}, vector A n → vector B n → vector C n
|
||||
| map nil nil := nil
|
||||
| map (a :: va) (b :: vb) := f a b :: map va vb
|
||||
|
|
|
|||
|
|
@ -1,9 +1,9 @@
|
|||
open nat
|
||||
|
||||
theorem lt_trans : ∀ {a b c : nat}, a < b → b < c → a < c,
|
||||
lt_trans h (lt.base _) := lt.step h,
|
||||
lt_trans h₁ (lt.step h₂) := lt.step (lt_trans h₁ h₂)
|
||||
theorem lt_trans : ∀ {a b c : nat}, a < b → b < c → a < c
|
||||
| lt_trans h (lt.base _) := lt.step h
|
||||
| lt_trans h₁ (lt.step h₂) := lt.step (lt_trans h₁ h₂)
|
||||
|
||||
theorem lt_succ : ∀ {a b : nat}, a < b → succ a < succ b,
|
||||
lt_succ (lt.base a) := lt.base (succ a),
|
||||
lt_succ (lt.step h) := lt.step (lt_succ h)
|
||||
theorem lt_succ : ∀ {a b : nat}, a < b → succ a < succ b
|
||||
| lt_succ (lt.base a) := lt.base (succ a)
|
||||
| lt_succ (lt.step h) := lt.step (lt_succ h)
|
||||
|
|
|
|||
|
|
@ -1,15 +1,15 @@
|
|||
open nat
|
||||
|
||||
definition foo : nat → nat,
|
||||
foo zero := begin exact zero end,
|
||||
foo (succ a) := begin exact a end
|
||||
definition foo : nat → nat
|
||||
| foo zero := begin exact zero end
|
||||
| foo (succ a) := begin exact a end
|
||||
|
||||
example : foo zero = zero := rfl
|
||||
example (a : nat) : foo (succ a) = a := rfl
|
||||
|
||||
definition bla : nat → nat,
|
||||
bla zero := zero,
|
||||
bla (succ a) :=
|
||||
definition bla : nat → nat
|
||||
| bla zero := zero
|
||||
| bla (succ a) :=
|
||||
begin
|
||||
apply foo,
|
||||
exact a
|
||||
|
|
|
|||
|
|
@ -14,18 +14,18 @@ fz : Π n, fin (succ n),
|
|||
fs : Π {n}, fin n → fin (succ n)
|
||||
|
||||
namespace fin
|
||||
definition to_nat : Π {n}, fin n → nat,
|
||||
to_nat (fz n) := zero,
|
||||
to_nat (@fs n f) := succ (@to_nat n f)
|
||||
definition to_nat : Π {n}, fin n → nat
|
||||
| to_nat (fz n) := zero
|
||||
| to_nat (@fs n f) := succ (@to_nat n f)
|
||||
|
||||
definition lift : Π {n : nat}, fin n → Π (m : nat), fin (add m n),
|
||||
lift (fz n) m := fz (add m n),
|
||||
lift (@fs n f) m := fs (@lift n f m)
|
||||
definition lift : Π {n : nat}, fin n → Π (m : nat), fin (add m n)
|
||||
| lift (fz n) m := fz (add m n)
|
||||
| lift (@fs n f) m := fs (@lift n f m)
|
||||
|
||||
theorem to_nat_lift : ∀ {n : nat} (f : fin n) (m : nat), to_nat f = to_nat (lift f m),
|
||||
to_nat_lift (fz n) m := rfl,
|
||||
to_nat_lift (@fs n f) m := calc
|
||||
to_nat (fs f) = (to_nat f) + 1 : rfl
|
||||
... = (to_nat (lift f m)) + 1 : to_nat_lift f
|
||||
... = to_nat (lift (fs f) m) : rfl
|
||||
theorem to_nat_lift : ∀ {n : nat} (f : fin n) (m : nat), to_nat f = to_nat (lift f m)
|
||||
| to_nat_lift (fz n) m := rfl
|
||||
| to_nat_lift (@fs n f) m := calc
|
||||
to_nat (fs f) = (to_nat f) + 1 : rfl
|
||||
... = (to_nat (lift f m)) + 1 : to_nat_lift f
|
||||
... = to_nat (lift (fs f) m) : rfl
|
||||
end fin
|
||||
|
|
|
|||
|
|
@ -14,18 +14,18 @@ fz : Π n, fin (succ n),
|
|||
fs : Π {n}, fin n → fin (succ n)
|
||||
|
||||
namespace fin
|
||||
definition to_nat : Π {n}, fin n → nat,
|
||||
@to_nat (succ n) (fz n) := zero,
|
||||
@to_nat (succ n) (fs f) := succ (@to_nat n f)
|
||||
definition to_nat : Π {n}, fin n → nat
|
||||
| @to_nat (succ n) (fz n) := zero
|
||||
| @to_nat (succ n) (fs f) := succ (@to_nat n f)
|
||||
|
||||
definition lift : Π {n : nat}, fin n → Π (m : nat), fin (add m n),
|
||||
@lift (succ n) (fz n) m := fz (add m n),
|
||||
@lift (succ n) (@fs n f) m := fs (@lift n f m)
|
||||
definition lift : Π {n : nat}, fin n → Π (m : nat), fin (add m n)
|
||||
| @lift (succ n) (fz n) m := fz (add m n)
|
||||
| @lift (succ n) (@fs n f) m := fs (@lift n f m)
|
||||
|
||||
theorem to_nat_lift : ∀ {n : nat} (f : fin n) (m : nat), to_nat f = to_nat (lift f m),
|
||||
to_nat_lift (fz n) m := rfl,
|
||||
to_nat_lift (@fs n f) m := calc
|
||||
to_nat (fs f) = (to_nat f) + 1 : rfl
|
||||
... = (to_nat (lift f m)) + 1 : to_nat_lift f
|
||||
... = to_nat (lift (fs f) m) : rfl
|
||||
theorem to_nat_lift : ∀ {n : nat} (f : fin n) (m : nat), to_nat f = to_nat (lift f m)
|
||||
| to_nat_lift (fz n) m := rfl
|
||||
| to_nat_lift (@fs n f) m := calc
|
||||
to_nat (fs f) = (to_nat f) + 1 : rfl
|
||||
... = (to_nat (lift f m)) + 1 : to_nat_lift f
|
||||
... = to_nat (lift (fs f) m) : rfl
|
||||
end fin
|
||||
|
|
|
|||
|
|
@ -3,22 +3,22 @@ open nat
|
|||
|
||||
definition foo (a : nat) : nat :=
|
||||
match a with
|
||||
zero := zero,
|
||||
succ n := n
|
||||
| zero := zero
|
||||
| succ n := n
|
||||
end
|
||||
|
||||
example : foo 3 = 2 := rfl
|
||||
|
||||
open decidable
|
||||
|
||||
protected theorem dec_eq : ∀ x y : nat, decidable (x = y),
|
||||
dec_eq zero zero := inl rfl,
|
||||
dec_eq (succ x) zero := inr (λ h, nat.no_confusion h),
|
||||
dec_eq zero (succ y) := inr (λ h, nat.no_confusion h),
|
||||
dec_eq (succ x) (succ y) :=
|
||||
protected theorem dec_eq : ∀ x y : nat, decidable (x = y)
|
||||
| dec_eq zero zero := inl rfl
|
||||
| dec_eq (succ x) zero := inr (λ h, nat.no_confusion h)
|
||||
| dec_eq zero (succ y) := inr (λ h, nat.no_confusion h)
|
||||
| dec_eq (succ x) (succ y) :=
|
||||
match dec_eq x y with
|
||||
inl H := inl (eq.rec_on H rfl),
|
||||
inr H := inr (λ h : succ x = succ y, nat.no_confusion h (λ heq : x = y, absurd heq H))
|
||||
| inl H := inl (eq.rec_on H rfl)
|
||||
| inr H := inr (λ h : succ x = succ y, nat.no_confusion h (λ heq : x = y, absurd heq H))
|
||||
end
|
||||
|
||||
context
|
||||
|
|
@ -28,12 +28,12 @@ context
|
|||
parameter [H : decidable_pred p]
|
||||
include H
|
||||
|
||||
definition filter : list A → list A,
|
||||
filter nil := nil,
|
||||
filter (a :: l) :=
|
||||
definition filter : list A → list A
|
||||
| filter nil := nil
|
||||
| filter (a :: l) :=
|
||||
match H a with
|
||||
inl h := a :: filter l,
|
||||
inr h := filter l
|
||||
| inl h := a :: filter l
|
||||
| inr h := filter l
|
||||
end
|
||||
|
||||
theorem filter_nil : filter nil = nil :=
|
||||
|
|
@ -45,9 +45,9 @@ end
|
|||
|
||||
definition sub2 (a : nat) : nat :=
|
||||
match a with
|
||||
0 := 0,
|
||||
1 := 0,
|
||||
b+2 := b
|
||||
| 0 := 0
|
||||
| 1 := 0
|
||||
| b+2 := b
|
||||
end
|
||||
|
||||
example (a : nat) : sub2 (succ (succ a)) = a := rfl
|
||||
|
|
|
|||
|
|
@ -2,10 +2,10 @@ open nat bool inhabited prod
|
|||
|
||||
definition diag (a b c : bool) : nat :=
|
||||
match (a, b, c) with
|
||||
(_, tt, ff) := 1,
|
||||
(ff, _, tt) := 2,
|
||||
(tt, ff, _) := 3,
|
||||
(_, _, _) := arbitrary nat
|
||||
| (_, tt, ff) := 1
|
||||
| (ff, _, tt) := 2
|
||||
| (tt, ff, _) := 3
|
||||
| (_, _, _) := arbitrary nat
|
||||
end
|
||||
|
||||
theorem diag1 (a : bool) : diag a tt ff = 1 :=
|
||||
|
|
|
|||
|
|
@ -10,8 +10,8 @@ match x with
|
|||
⟨a, b, h⟩ := a
|
||||
end
|
||||
|
||||
definition src2 {A B : Type} : arrow_ob A B → A,
|
||||
src2 ⟨a, _, _⟩ := a
|
||||
definition src2 {A B : Type} : arrow_ob A B → A
|
||||
| src2 ⟨a, _, _⟩ := a
|
||||
|
||||
definition src3 {A B : Type} (x : arrow_ob A B) : A :=
|
||||
match x with
|
||||
|
|
|
|||
|
|
@ -3,9 +3,9 @@ open nat vector prod
|
|||
|
||||
variables {A B : Type}
|
||||
|
||||
definition unzip : Π {n : nat}, vector (A × B) n → vector A n × vector B n,
|
||||
@unzip ⌞zero⌟ nil := (nil, nil),
|
||||
@unzip ⌞succ n⌟ ((a, b) :: v) :=
|
||||
definition unzip : Π {n : nat}, vector (A × B) n → vector A n × vector B n
|
||||
| @unzip ⌞zero⌟ nil := (nil, nil)
|
||||
| @unzip ⌞succ n⌟ ((a, b) :: v) :=
|
||||
match unzip v with
|
||||
(va, vb) := (a :: va, b :: vb)
|
||||
end
|
||||
|
|
|
|||
|
|
@ -3,6 +3,6 @@ open nat
|
|||
variable a : nat
|
||||
|
||||
-- The variable 'a' in the following definition is not the variable 'a' above
|
||||
definition tadd : nat → nat → nat,
|
||||
tadd zero b := b,
|
||||
tadd (succ a) b := succ (tadd a b)
|
||||
definition tadd : nat → nat → nat
|
||||
| tadd zero b := b
|
||||
| tadd (succ a) b := succ (tadd a b)
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
shadow.lean:8:11: error: invalid recursive equation, variable 'a' has the same name of a variable in an outer-scope (solution: rename this variable)
|
||||
shadow.lean:8:13: error: invalid recursive equation, variable 'a' has the same name of a variable in an outer-scope (solution: rename this variable)
|
||||
|
|
|
|||
|
|
@ -3,9 +3,9 @@ open nat vector prod
|
|||
|
||||
variables {A B : Type}
|
||||
|
||||
definition unzip : Π {n : nat}, vector (A × B) n → vector A n × vector B n,
|
||||
unzip nil := (nil, nil),
|
||||
unzip ((a, b) :: v) :=
|
||||
definition unzip : Π {n : nat}, vector (A × B) n → vector A n × vector B n
|
||||
| unzip nil := (nil, nil)
|
||||
| unzip ((a, b) :: v) :=
|
||||
match unzip v with
|
||||
(va, vb) := (a :: va, b :: vb)
|
||||
end
|
||||
|
|
|
|||
Loading…
Reference in a new issue