michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(kernel/inductive): replace recursor name, use '.rec' instead of '_rec'

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-09-04 15:03:59 -07:00
parent 653141135d
commit 8743394627
100 changed files with 322 additions and 328 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
library/data/bool.lean
View file

@ -13,13 +13,13 @@ tt : bool
namespace bool
theorem cases_on {p : bool → Prop} (b : bool) (H0 : p ff) (H1 : p tt) : p b :=
bool_rec H0 H1 b
rec H0 H1 b
theorem bool_inhabited [instance] : inhabited bool :=
inhabited_mk ff
definition cond {A : Type} (b : bool) (t e : A) :=
bool_rec e t b
rec e t b
theorem dichotomy (b : bool) : b = ff ∨ b = tt :=
cases_on b (or_inl (refl ff)) (or_inr (refl tt))
@ -38,13 +38,13 @@ assume H : ff = tt, absurd
true_ne_false
theorem decidable_eq [instance] (a b : bool) : decidable (a = b) :=
bool_rec
(bool_rec (inl (refl ff)) (inr ff_ne_tt) b)
(bool_rec (inr (ne_symm ff_ne_tt)) (inl (refl tt)) b)
rec
(rec (inl (refl ff)) (inr ff_ne_tt) b)
(rec (inr (ne_symm ff_ne_tt)) (inl (refl tt)) b)
a
definition bor (a b : bool) :=
bool_rec (bool_rec ff tt b) tt a
rec (rec ff tt b) tt a
theorem bor_tt_left (a : bool) : bor tt a = tt :=
rfl
@ -77,7 +77,7 @@ cases_on a
... = tt || (b || c) : bor_tt_left (b || c)⁻¹)
theorem bor_to_or {a b : bool} : a || b = tt → a = tt ∨ b = tt :=
bool_rec
rec
(assume H : ff || b = tt,
have Hb : b = tt, from (bor_ff_left b) ▸ H,
or_inr Hb)
@ -85,7 +85,7 @@ bool_rec
a
definition band (a b : bool) :=
bool_rec ff (bool_rec ff tt b) a
rec ff (rec ff tt b) a
infixl `&&` := band
@ -130,7 +130,7 @@ or_elim (dichotomy a)
theorem band_eq_tt_elim_right {a b : bool} (H : a && b = tt) : b = tt :=
band_eq_tt_elim_left (trans (band_comm b a) H)
definition bnot (a : bool) := bool_rec tt ff a
definition bnot (a : bool) := rec tt ff a
notation `!` x:max := bnot x

2
library/data/empty.lean
View file

@ -9,4 +9,4 @@
inductive empty : Type
theorem empty_elim (A : Type) (H : empty) : A := empty_rec (λe, A) H
theorem empty_elim (A : Type) (H : empty) : A := empty.rec (λe, A) H

29
library/data/list/basic.lean
View file

@ -18,15 +18,14 @@ open nat
open eq_ops
open helper_tactics
namespace list
-- Type
-- ----
inductive list (T : Type) : Type :=
nil {} : list T,
cons : T → list T → list T
namespace list
-- Type
-- ----
infix `::` := cons
section
@ -35,7 +34,7 @@ variable {T : Type}
theorem induction_on [protected] {P : list T → Prop} (l : list T) (Hnil : P nil)
(Hind : forall x : T, forall l : list T, forall H : P l, P (cons x l)) : P l :=
list_rec Hnil Hind l
rec Hnil Hind l
theorem cases_on [protected] {P : list T → Prop} (l : list T) (Hnil : P nil)
(Hcons : forall x : T, forall l : list T, P (cons x l)) : P l :=
@ -48,7 +47,7 @@ notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l
-- ------
definition concat (s t : list T) : list T :=
list_rec t (fun x : T, fun l : list T, fun u : list T, cons x u) s
rec t (fun x : T, fun l : list T, fun u : list T, cons x u) s
infixl `++` : 65 := concat
@ -73,7 +72,7 @@ induction_on s rfl
-- Length
-- ------
definition length : list T → ℕ := list_rec 0 (fun x l m, succ m)
definition length : list T → ℕ := rec 0 (fun x l m, succ m)
theorem length_nil : length (@nil T) = 0 := rfl
@ -98,7 +97,7 @@ induction_on s
-- Append
-- ------
definition append (x : T) : list T → list T := list_rec [x] (fun y l l', y :: l')
definition append (x : T) : list T → list T := rec [x] (fun y l l', y :: l')
theorem append_nil {x : T} : append x nil = [x]
@ -111,7 +110,7 @@ theorem append_eq_concat {x : T} {l : list T} : append x l = l ++ [x]
-- Reverse
-- -------
definition reverse : list T → list T := list_rec nil (fun x l r, r ++ [x])
definition reverse : list T → list T := rec nil (fun x l r, r ++ [x])
theorem reverse_nil : reverse (@nil T) = nil
@ -153,7 +152,7 @@ induction_on l rfl
-- Head and tail
-- -------------
definition head (x : T) : list T → T := list_rec x (fun x l h, x)
definition head (x : T) : list T → T := rec x (fun x l h, x)
theorem head_nil {x : T} : head x (@nil T) = x
@ -168,7 +167,7 @@ cases_on s
... = x : {head_cons}
... = head x (cons x s) : {head_cons⁻¹})
definition tail : list T → list T := list_rec nil (fun x l b, l)
definition tail : list T → list T := rec nil (fun x l b, l)
theorem tail_nil : tail (@nil T) = nil
@ -182,7 +181,7 @@ cases_on l
-- List membership
-- ---------------
definition mem (x : T) : list T → Prop := list_rec false (fun y l H, x = y ∨ H)
definition mem (x : T) : list T → Prop := rec false (fun y l H, x = y ∨ H)
infix `∈` := mem
@ -238,7 +237,7 @@ induction_on l
-- to do this: need decidability of = for nat
-- definition find (x : T) : list T → nat
-- := list_rec 0 (fun y l b, if x = y then 0 else succ b)
-- := rec 0 (fun y l b, if x = y then 0 else succ b)
-- theorem find_nil (f : T) : find f nil = 0
-- :=refl _
@ -272,7 +271,7 @@ induction_on l
-- -----------
definition nth (x : T) (l : list T) (n : ℕ) : T :=
nat_rec (λl, head x l) (λm f l, f (tail l)) n l
nat.rec (λl, head x l) (λm f l, f (tail l)) n l
theorem nth_zero {x : T} {l : list T} : nth x l 0 = head x l

26
library/data/nat/basic.lean
View file

@ -16,36 +16,36 @@ open helper_tactics
-- Definition of the type
-- ----------------------
namespace nat
inductive nat : Type :=
zero : nat,
succ : nat → nat
namespace nat
notation `ℕ` := nat
theorem rec_zero {P : ℕ → Type} (x : P zero) (f : ∀m, P m → P (succ m)) : nat_rec x f zero = x
theorem rec_zero {P : ℕ → Type} (x : P zero) (f : ∀m, P m → P (succ m)) : nat.rec x f zero = x
theorem rec_succ {P : ℕ → Type} (x : P zero) (f : ∀m, P m → P (succ m)) (n : ℕ) :
nat_rec x f (succ n) = f n (nat_rec x f n)
nat.rec x f (succ n) = f n (nat.rec x f n)
theorem induction_on [protected] {P : ℕ → Prop} (a : ℕ) (H1 : P zero) (H2 : ∀ (n : ℕ) (IH : P n), P (succ n)) :
P a :=
nat_rec H1 H2 a
nat.rec H1 H2 a
definition rec_on [protected] {P : ℕ → Type} (n : ℕ) (H1 : P zero) (H2 : ∀m, P m → P (succ m)) : P n :=
nat_rec H1 H2 n
nat.rec H1 H2 n
-- Coercion from num
-- -----------------
abbreviation plus (x y : ℕ) : ℕ :=
nat_rec x (λ n r, succ r) y
nat.rec x (λ n r, succ r) y
definition to_nat [coercion] [inline] (n : num) : ℕ :=
num_rec zero
(λ n, pos_num_rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n
num.num.rec zero
(λ n, num.pos_num.rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n
-- Successor and predecessor
@ -54,7 +54,7 @@ num_rec zero
theorem succ_ne_zero {n : ℕ} : succ n ≠ 0 :=
assume H : succ n = 0,
have H2 : true = false, from
let f := (nat_rec false (fun a b, true)) in
let f := (nat.rec false (fun a b, true)) in
calc
true = f (succ n) : rfl
... = f 0 : {H}
@ -63,7 +63,7 @@ absurd H2 true_ne_false
-- add_rewrite succ_ne_zero
definition pred (n : ℕ) := nat_rec 0 (fun m x, m) n
definition pred (n : ℕ) := nat.rec 0 (fun m x, m) n
theorem pred_zero : pred 0 = 0
@ -255,12 +255,12 @@ add_zero_left ▸ add_succ_left
-- TODO: rename? remove?
theorem induction_plus_one {P : nat → Prop} (a : ℕ) (H1 : P 0)
(H2 : ∀ (n : ℕ) (IH : P n), P (n + 1)) : P a :=
nat_rec H1 (take n IH, add_one ▸ (H2 n IH)) a
nat.rec H1 (take n IH, add_one ▸ (H2 n IH)) a
-- Multiplication
-- --------------
definition mul (n m : ℕ) := nat_rec 0 (fun m x, x + n) m
definition mul (n m : ℕ) := nat.rec 0 (fun m x, x + n) m
infixl `*` := mul
theorem mul_zero_right {n : ℕ} : n * 0 = 0

2
library/data/nat/div.lean
View file

@ -54,7 +54,7 @@ if_neg H
definition rec_measure_aux {dom codom : Type} (default : codom) (measure : dom → ℕ)
(rec_val : dom → (dom → codom) → codom) : ℕ → dom → codom :=
nat_rec (λx, default) (λm g x, if measure x < succ m then rec_val x g else default)
rec (λx, default) (λm g x, if measure x < succ m then rec_val x g else default)
definition rec_measure {dom codom : Type} (default : codom) (measure : dom → ℕ)
(rec_val : dom → (dom → codom) → codom) (x : dom) : codom :=

1
library/data/nat/order.lean
View file

@ -12,7 +12,6 @@ import tools.fake_simplifier
open nat eq_ops tactic
open fake_simplifier
open decidable (decidable inl inr)
namespace nat

2
library/data/nat/sub.lean
View file

@ -19,7 +19,7 @@ namespace nat
-- subtraction
-- -----------
definition sub (n m : ℕ) : nat := nat_rec n (fun m x, pred x) m
definition sub (n m : ℕ) : nat := rec n (fun m x, pred x) m
infixl `-` := sub
theorem sub_zero_right {n : ℕ} : n - 0 = n

1
library/data/num.lean
View file

@ -7,7 +7,6 @@
import logic.classes.inhabited
namespace num
-- pos_num and num are two auxiliary datatypes used when parsing numerals such as 13, 0, 26.
-- The parser will generate the terms (pos (bit1 (bit1 (bit0 one)))), zero, and (pos (bit0 (bit1 (bit1 one)))).
-- This representation can be coerced in whatever we want (e.g., naturals, integers, reals, etc).

8
library/data/option.lean
View file

@ -13,14 +13,14 @@ some : A → option A
theorem induction_on [protected] {A : Type} {p : option A → Prop} (o : option A)
(H1 : p none) (H2 : ∀a, p (some a)) : p o :=
option_rec H1 H2 o
option.rec H1 H2 o
definition rec_on [protected] {A : Type} {C : option A → Type} (o : option A)
(H1 : C none) (H2 : ∀a, C (some a)) : C o :=
option_rec H1 H2 o
option.rec H1 H2 o
definition is_none {A : Type} (o : option A) : Prop :=
option_rec true (λ a, false) o
option.rec true (λ a, false) o
theorem is_none_none {A : Type} : is_none (@none A) :=
trivial
@ -34,7 +34,7 @@ assume H : none = some a, absurd
(not_is_none_some a)
theorem some_inj {A : Type} {a₁ a₂ : A} (H : some a₁ = some a₂) : a₁ = a₂ :=
congr_arg (option_rec a₁ (λ a, a)) H
congr_arg (option.rec a₁ (λ a, a)) H
theorem option_inhabited [instance] (A : Type) : inhabited (option A) :=
inhabited_mk none

13
library/data/prod.lean
View file

@ -25,8 +25,8 @@ section
parameters {A B : Type}
abbreviation pr1 (p : prod A B) := prod_rec (λ x y, x) p
abbreviation pr2 (p : prod A B) := prod_rec (λ x y, y) p
abbreviation pr1 (p : prod A B) := rec (λ x y, x) p
abbreviation pr2 (p : prod A B) := rec (λ x y, y) p
theorem pr1_pair (a : A) (b : B) : pr1 (a, b) = a :=
rfl
@ -34,18 +34,17 @@ section
theorem pr2_pair (a : A) (b : B) : pr2 (a, b) = b :=
rfl
-- TODO: remove prefix when we can protect it
theorem pair_destruct {P : A × B → Prop} (p : A × B) (H : ∀a b, P (a, b)) : P p :=
prod_rec H p
theorem destruct [protected] {P : A × B → Prop} (p : A × B) (H : ∀a b, P (a, b)) : P p :=
rec H p
theorem prod_ext (p : prod A B) : pair (pr1 p) (pr2 p) = p :=
pair_destruct p (λx y, refl (x, y))
destruct p (λx y, refl (x, y))
theorem pair_eq {a1 a2 : A} {b1 b2 : B} (H1 : a1 = a2) (H2 : b1 = b2) : (a1, b1) = (a2, b2) :=
subst H1 (subst H2 rfl)
theorem prod_eq {p1 p2 : prod A B} : ∀ (H1 : pr1 p1 = pr1 p2) (H2 : pr2 p1 = pr2 p2), p1 = p2 :=
pair_destruct p1 (take a1 b1, pair_destruct p2 (take a2 b2 H1 H2, pair_eq H1 H2))
destruct p1 (take a1 b1, destruct p2 (take a2 b2 H1 H2, pair_eq H1 H2))
theorem prod_inhabited [instance] (H1 : inhabited A) (H2 : inhabited B) : inhabited (prod A B) :=
inhabited_destruct H1 (λa, inhabited_destruct H2 (λb, inhabited_mk (pair a b)))

2
library/data/quotient/aux.lean
View file

@ -26,7 +26,7 @@ theorem flip_pr1 {A B : Type} (a : A × B) : pr1 (flip a) = pr2 a := rfl
theorem flip_pr2 {A B : Type} (a : A × B) : pr2 (flip a) = pr1 a := rfl
theorem flip_flip {A B : Type} (a : A × B) : flip (flip a) = a :=
pair_destruct a (take x y, rfl)
prod.destruct a (take x y, rfl)
theorem P_flip {A B : Type} {P : A → B → Prop} {a : A × B} (H : P (pr1 a) (pr2 a))
: P (pr2 (flip a)) (pr1 (flip a)) :=

2
library/data/quotient/basic.lean
View file

@ -222,7 +222,7 @@ theorem image_elt_of {A B : Type} {f : A → B} (u : image f) : ∃a, f a = elt_
has_property u
theorem fun_image_surj {A B : Type} {f : A → B} (u : image f) : ∃a, fun_image f a = u :=
subtype_destruct u
subtype.destruct u
(take (b : B) (H : ∃a, f a = b),
obtain a (H': f a = b), from H,
(exists_intro a (tag_eq H')))

8
library/data/sigma.lean
View file

@ -17,15 +17,15 @@ section
parameters {A : Type} {B : A → Type}
abbreviation dpr1 (p : Σ x, B x) : A := sigma_rec (λ a b, a) p
abbreviation dpr2 {A : Type} {B : A → Type} (p : Σ x, B x) : B (dpr1 p) := sigma_rec (λ a b, b) p
abbreviation dpr1 (p : Σ x, B x) : A := rec (λ a b, a) p
abbreviation dpr2 {A : Type} {B : A → Type} (p : Σ x, B x) : B (dpr1 p) := rec (λ a b, b) p
theorem dpr1_dpair (a : A) (b : B a) : dpr1 (dpair a b) = a := refl a
theorem dpr2_dpair (a : A) (b : B a) : dpr2 (dpair a b) = b := refl b
-- TODO: remove prefix when we can protect it
theorem sigma_destruct {P : sigma B → Prop} (p : sigma B) (H : ∀a b, P (dpair a b)) : P p :=
sigma_rec H p
rec H p
theorem dpair_ext (p : sigma B) : dpair (dpr1 p) (dpr2 p) = p :=
sigma_destruct p (take a b, rfl)
@ -34,7 +34,7 @@ section
theorem dpair_eq {a1 a2 : A} {b1 : B a1} {b2 : B a2} (H1 : a1 = a2) (H2 : eq_rec_on H1 b1 = b2) :
dpair a1 b1 = dpair a2 b2 :=
(show ∀(b2 : B a2) (H1 : a1 = a2) (H2 : eq_rec_on H1 b1 = b2), dpair a1 b1 = dpair a2 b2, from
eq_rec
eq.rec
(take (b2' : B a1),
assume (H1' : a1 = a1),
assume (H2' : eq_rec_on H1' b1 = b2'),

19
library/data/subtype.lean
View file

@ -18,31 +18,31 @@ section
parameter {P : A → Prop}
-- TODO: make this a coercion?
definition elt_of (a : {x, P x}) : A := subtype_rec (λ x y, x) a
theorem has_property (a : {x, P x}) : P (elt_of a) := subtype_rec (λ x y, y) a
definition elt_of (a : {x, P x}) : A := rec (λ x y, x) a
theorem has_property (a : {x, P x}) : P (elt_of a) := rec (λ x y, y) a
theorem elt_of_tag (a : A) (H : P a) : elt_of (tag a H) = a := refl a
theorem subtype_destruct {Q : {x, P x} → Prop} (a : {x, P x})
theorem destruct [protected] {Q : {x, P x} → Prop} (a : {x, P x})
(H : ∀(x : A) (H1 : P x), Q (tag x H1)) : Q a :=
subtype_rec H a
rec H a
theorem tag_irrelevant {a : A} (H1 H2 : P a) : tag a H1 = tag a H2 :=
rfl
theorem tag_elt_of (a : subtype P) : ∀(H : P (elt_of a)), tag (elt_of a) H = a :=
subtype_destruct a (take (x : A) (H1 : P x) (H2 : P x), rfl)
destruct a (take (x : A) (H1 : P x) (H2 : P x), rfl)
theorem tag_eq {a1 a2 : A} {H1 : P a1} {H2 : P a2} (H3 : a1 = a2) : tag a1 H1 = tag a2 H2 :=
subst H3 (take H2, tag_irrelevant H1 H2) H2
theorem subtype_eq {a1 a2 : {x, P x}} : ∀(H : elt_of a1 = elt_of a2), a1 = a2 :=
subtype_destruct a1 (take x1 H1, subtype_destruct a2 (take x2 H2 H, tag_eq H))
destruct a1 (take x1 H1, destruct a2 (take x2 H2 H, tag_eq H))
theorem subtype_inhabited {a : A} (H : P a) : inhabited {x, P x} :=
theorem subtype_inhabited [instance] {a : A} (H : P a) : inhabited {x, P x} :=
inhabited_mk (tag a H)
theorem subtype_eq_decidable (a1 a2 : {x, P x})
theorem eq_decidable [protected] [instance] (a1 a2 : {x, P x})
(H : decidable (elt_of a1 = elt_of a2)) : decidable (a1 = a2) :=
have H1 : (a1 = a2) ↔ (elt_of a1 = elt_of a2), from
iff_intro (assume H, subst H rfl) (assume H, subtype_eq H),
@ -50,7 +50,4 @@ section
end
instance subtype_inhabited
instance subtype_eq_decidable
end subtype

4
library/data/sum.lean
View file

@ -26,11 +26,11 @@ end sum_plus_notation
abbreviation rec_on [protected] {A B : Type} {C : (A ⊎ B) → Type} (s : A ⊎ B)
(H1 : ∀a : A, C (inl B a)) (H2 : ∀b : B, C (inr A b)) : C s :=
sum_rec H1 H2 s
rec H1 H2 s
abbreviation cases_on [protected] {A B : Type} {P : (A ⊎ B) → Prop} (s : A ⊎ B)
(H1 : ∀a : A, P (inl B a)) (H2 : ∀b : B, P (inr A b)) : P s :=
sum_rec H1 H2 s
rec H1 H2 s
-- Here is the trick for the theorems that follow:
-- Fixing a1, "f s" is a recursive description of "inl B a1 = s".

2
library/data/unit.lean
View file

@ -14,7 +14,7 @@ star : unit
notation `⋆`:max := star
theorem unit_eq (a b : unit) : a = b :=
unit_rec (unit_rec (refl ⋆) b) a
rec (rec rfl b) a
theorem unit_eq_star (a : unit) : a = star :=
unit_eq a star

12
library/hott/equiv.lean
View file

@ -24,18 +24,18 @@ IsEquiv_mk : Π
IsEquiv f
definition equiv_inv {A B : Type} {f : A → B} (H : IsEquiv f) : B → A :=
IsEquiv_rec (λequiv_inv eisretr eissect eisadj, equiv_inv) H
IsEquiv.rec (λequiv_inv eisretr eissect eisadj, equiv_inv) H
-- TODO: note: does not type check without giving the type
definition eisretr {A B : Type} {f : A → B} (H : IsEquiv f) : Sect (equiv_inv H) f :=
IsEquiv_rec (λequiv_inv eisretr eissect eisadj, eisretr) H
IsEquiv.rec (λequiv_inv eisretr eissect eisadj, eisretr) H
definition eissect {A B : Type} {f : A → B} (H : IsEquiv f) : Sect f (equiv_inv H) :=
IsEquiv_rec (λequiv_inv eisretr eissect eisadj, eissect) H
IsEquiv.rec (λequiv_inv eisretr eissect eisadj, eissect) H
definition eisadj {A B : Type} {f : A → B} (H : IsEquiv f) :
Πx, eisretr H (f x) ≈ ap f (eissect H x) :=
IsEquiv_rec (λequiv_inv eisretr eissect eisadj, eisadj) H
IsEquiv.rec (λequiv_inv eisretr eissect eisadj, eisadj) H
-- Structure Equiv
@ -46,13 +46,13 @@ Equiv_mk : Π
Equiv A B
definition equiv_fun {A B : Type} (e : Equiv A B) : A → B :=
Equiv_rec (λequiv_fun equiv_isequiv, equiv_fun) e
Equiv.rec (λequiv_fun equiv_isequiv, equiv_fun) e
-- TODO: use a type class instead?
coercion equiv_fun : Equiv
definition equiv_isequiv [coercion] {A B : Type} (e : Equiv A B) : IsEquiv (equiv_fun e) :=
Equiv_rec (λequiv_fun equiv_isequiv, equiv_isequiv) e
Equiv.rec (λequiv_fun equiv_isequiv, equiv_isequiv) e
-- coercion equiv_isequiv

6
library/hott/path.lean
View file

@ -25,7 +25,7 @@ notation `idp`:max := idpath _ -- TODO: can we / should we use `1`?
namespace path
abbreviation induction_on [protected] {A : Type} {a b : A} (p : a ≈ b)
{C : Π (b : A) (p : a ≈ b), Type} (H : C a (idpath a)) : C b p :=
path_rec H p
path.rec H p
end path
@ -36,11 +36,11 @@ open path (induction_on)
-- -------------------------
definition concat {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : x ≈ z :=
path_rec (λu, u) q p
path.rec (λu, u) q p
-- TODO: should this be an abbreviation?
definition inverse {A : Type} {x y : A} (p : x ≈ y) : y ≈ x :=
path_rec (idpath x) p
path.rec (idpath x) p
infixl `@`:75 := concat
postfix `^`:100 := inverse

8
library/hott/trunc.lean
View file

@ -15,10 +15,10 @@ Contr_mk : Π
(contr : Πy : A, center ≈ y),
Contr A
definition center {A : Type} (C : Contr A) : A := Contr_rec (λcenter contr, center) C
definition center {A : Type} (C : Contr A) : A := Contr.rec (λcenter contr, center) C
definition contr {A : Type} (C : Contr A) : Πy : A, center C ≈ y :=
Contr_rec (λcenter contr, contr) C
Contr.rec (λcenter contr, contr) C
inductive trunc_index : Type :=
minus_two : trunc_index,
@ -28,11 +28,11 @@ trunc_S : trunc_index → trunc_index
-- TODO: note in the Coq version, there is an internal version
definition IsTrunc (n : trunc_index) : Type → Type :=
trunc_index_rec (λA, Contr A) (λn trunc_n A, (Π(x y : A), trunc_n (x ≈ y))) n
trunc_index.rec (λA, Contr A) (λn trunc_n A, (Π(x y : A), trunc_n (x ≈ y))) n
-- TODO: in the Coq version, this is notation
abbreviation minus_one := trunc_S minus_two
abbreviation IsHProp := IsTrunc minus_one
abbreviation IsHSet := IsTrunc (trunc_S minus_one)
prefix `!`:75 := center
prefix `!`:75 := center

14
library/logic/classes/decidable.lean
View file

@ -4,12 +4,12 @@
import logic.core.connectives
namespace decidable
inductive decidable (p : Prop) : Type :=
inl : p → decidable p,
inr : ¬p → decidable p
namespace decidable
theorem true_decidable [instance] : decidable true :=
inl trivial
@ -17,19 +17,19 @@ theorem false_decidable [instance] : decidable false :=
inr not_false_trivial
theorem induction_on [protected] {p : Prop} {C : Prop} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C :=
decidable_rec H1 H2 H
decidable.rec H1 H2 H
definition rec_on [protected] [inline] {p : Prop} {C : Type} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) :
C :=
decidable_rec H1 H2 H
decidable.rec H1 H2 H
theorem irrelevant {p : Prop} (d1 d2 : decidable p) : d1 = d2 :=
decidable_rec
(assume Hp1 : p, decidable_rec
decidable.rec
(assume Hp1 : p, decidable.rec
(assume Hp2 : p, congr_arg inl (refl Hp1)) -- using proof irrelevance for Prop
(assume Hnp2 : ¬p, absurd Hp1 Hnp2)
d2)
(assume Hnp1 : ¬p, decidable_rec
(assume Hnp1 : ¬p, decidable.rec
(assume Hp2 : p, absurd Hp2 Hnp1)
(assume Hnp2 : ¬p, congr_arg inr (refl Hnp1)) -- using proof irrelevance for Prop
d2)

2
library/logic/classes/inhabited.lean
View file

@ -10,7 +10,7 @@ inhabited_mk : A → inhabited A
namespace inhabited
definition inhabited_destruct {A : Type} {B : Type} (H1 : inhabited A) (H2 : A → B) : B :=
inhabited_rec H2 H1
inhabited.rec H2 H1
definition Prop_inhabited [instance] : inhabited Prop :=
inhabited_mk true

2
library/logic/classes/nonempty.lean
View file

@ -12,7 +12,7 @@ inductive nonempty (A : Type) : Prop :=
nonempty_intro : A → nonempty A
definition nonempty_elim {A : Type} {B : Prop} (H1 : nonempty A) (H2 : A → B) : B :=
nonempty_rec H2 H1
nonempty.rec H2 H1
theorem inhabited_imp_nonempty [instance] {A : Type} (H : inhabited A) : nonempty A :=
nonempty_intro (default A)

2
library/logic/core/cast.lean
View file

@ -9,7 +9,7 @@ import .eq .quantifiers
open eq_ops
definition cast {A B : Type} (H : A = B) (a : A) : B :=
eq_rec a H
eq.rec a H
theorem cast_refl {A : Type} (a : A) : cast (refl A) a = a :=
refl (cast (refl A) a)

10
library/logic/core/connectives.lean
View file

@ -14,13 +14,13 @@ infixr `/\` := and
infixr `∧` := and
theorem and_elim {a b c : Prop} (H1 : a ∧ b) (H2 : a → b → c) : c :=
and_rec H2 H1
and.rec H2 H1
theorem and_elim_left {a b : Prop} (H : a ∧ b) : a :=
and_rec (λa b, a) H
and.rec (λa b, a) H
theorem and_elim_right {a b : Prop} (H : a ∧ b) : b :=
and_rec (λa b, b) H
and.rec (λa b, b) H
theorem and_swap {a b : Prop} (H : a ∧ b) : b ∧ a :=
and_intro (and_elim_right H) (and_elim_left H)
@ -55,7 +55,7 @@ theorem or_inl {a b : Prop} (Ha : a) : a ∨ b := or_intro_left b Ha
theorem or_inr {a b : Prop} (Hb : b) : a ∨ b := or_intro_right a Hb
theorem or_elim {a b c : Prop} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c :=
or_rec H2 H3 H1
or.rec H2 H3 H1
theorem resolve_right {a b : Prop} (H1 : a ∨ b) (H2 : ¬a) : b :=
or_elim H1 (assume Ha, absurd Ha H2) (assume Hb, Hb)
@ -103,7 +103,7 @@ theorem iff_def {a b : Prop} : (a ↔ b) = ((a → b) ∧ (b → a)) := rfl
theorem iff_intro {a b : Prop} (H1 : a → b) (H2 : b → a) : a ↔ b := and_intro H1 H2
theorem iff_elim {a b c : Prop} (H1 : (a → b) → (b → a) → c) (H2 : a ↔ b) : c := and_rec H1 H2
theorem iff_elim {a b c : Prop} (H1 : (a → b) → (b → a) → c) (H2 : a ↔ b) : c := and.rec H1 H2
theorem iff_elim_left {a b : Prop} (H : a ↔ b) : a → b :=
iff_elim (assume H1 H2, H1) H

6
library/logic/core/eq.lean
View file

@ -23,7 +23,7 @@ theorem eq_id_refl {A : Type} {a : A} (H1 : a = a) : H1 = (refl a) := rfl
theorem eq_irrel {A : Type} {a b : A} (H1 H2 : a = b) : H1 = H2 := rfl
theorem subst {A : Type} {a b : A} {P : A → Prop} (H1 : a = b) (H2 : P a) : P b :=
eq_rec H2 H1
eq.rec H2 H1
theorem trans {A : Type} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c :=
subst H2 H1
@ -48,12 +48,12 @@ assume H : true = false,
-- eq_rec with arguments swapped, for transporting an element of a dependent type
definition eq_rec_on {A : Type} {a1 a2 : A} {B : A → Type} (H1 : a1 = a2) (H2 : B a1) : B a2 :=
eq_rec H2 H1
eq.rec H2 H1
theorem eq_rec_on_id {A : Type} {a : A} {B : A → Type} (H : a = a) (b : B a) : eq_rec_on H b = b :=
refl (eq_rec_on rfl b)
theorem eq_rec_id {A : Type} {a : A} {B : A → Type} (H : a = a) (b : B a) : eq_rec b H = b :=
theorem eq_rec_id {A : Type} {a : A} {B : A → Type} (H : a = a) (b : B a) : eq.rec b H = b :=
eq_rec_on_id H b
theorem eq_rec_on_compose {A : Type} {a b c : A} {P : A → Type} (H1 : a = b) (H2 : b = c)

6
library/logic/core/if.lean
View file

@ -13,19 +13,19 @@ decidable.rec_on H (assume Hc, t) (assume Hnc, e)
notation `if` c `then` t `else` e:45 := ite c t e
theorem if_pos {c : Prop} {H : decidable c} (Hc : c) {A : Type} {t e : A} : (if c then t else e) = t :=
decidable_rec
decidable.rec
(assume Hc : c, refl (@ite c (inl Hc) A t e))
(assume Hnc : ¬c, absurd Hc Hnc)
H
theorem if_neg {c : Prop} {H : decidable c} (Hnc : ¬c) {A : Type} {t e : A} : (if c then t else e) = e :=
decidable_rec
decidable.rec
(assume Hc : c, absurd Hc Hnc)
(assume Hnc : ¬c, refl (@ite c (inr Hnc) A t e))
H
theorem if_t_t (c : Prop) {H : decidable c} {A : Type} (t : A) : (if c then t else t) = t :=
decidable_rec
decidable.rec
(assume Hc : c, refl (@ite c (inl Hc) A t t))
(assume Hnc : ¬c, refl (@ite c (inr Hnc) A t t))
H

2
library/logic/core/prop.lean
View file

@ -19,7 +19,7 @@ abbreviation imp (a b : Prop) : Prop := a → b
inductive false : Prop
theorem false_elim {c : Prop} (H : false) : c :=
false_rec c H
false.rec c H
inductive true : Prop :=
trivial : true

2
library/logic/core/quantifiers.lean
View file

@ -13,7 +13,7 @@ notation `exists` binders `,` r:(scoped P, Exists P) := r
notation `∃` binders `,` r:(scoped P, Exists P) := r
theorem exists_elim {A : Type} {p : A → Prop} {B : Prop} (H1 : ∃x, p x) (H2 : ∀ (a : A) (H : p a), B) : B :=
Exists_rec H2 H1
Exists.rec H2 H1
theorem exists_not_forall {A : Type} {p : A → Prop} (H : ∃x, p x) : ¬∀x, ¬p x :=
assume H1 : ∀x, ¬p x,

32
library/struc/relation.lean
View file

@ -24,10 +24,10 @@ is_reflexive_mk : reflexive R → is_reflexive R
namespace is_reflexive
abbreviation app ⦃T : Type⦄ {R : T → T → Type} (C : is_reflexive R) : reflexive R :=
is_reflexive_rec (λu, u) C
is_reflexive.rec (λu, u) C
abbreviation infer ⦃T : Type⦄ (R : T → T → Type) {C : is_reflexive R} : reflexive R :=
is_reflexive_rec (λu, u) C
is_reflexive.rec (λu, u) C
end is_reflexive
@ -38,10 +38,10 @@ is_symmetric_mk : symmetric R → is_symmetric R
namespace is_symmetric
abbreviation app ⦃T : Type⦄ {R : T → T → Type} (C : is_symmetric R) : symmetric R :=
is_symmetric_rec (λu, u) C
is_symmetric.rec (λu, u) C
abbreviation infer ⦃T : Type⦄ (R : T → T → Type) {C : is_symmetric R} : symmetric R :=
is_symmetric_rec (λu, u) C
is_symmetric.rec (λu, u) C
end is_symmetric
@ -52,10 +52,10 @@ is_transitive_mk : transitive R → is_transitive R
namespace is_transitive
abbreviation app ⦃T : Type⦄ {R : T → T → Type} (C : is_transitive R) : transitive R :=
is_transitive_rec (λu, u) C
is_transitive.rec (λu, u) C
abbreviation infer ⦃T : Type⦄ (R : T → T → Type) {C : is_transitive R} : transitive R :=
is_transitive_rec (λu, u) C
is_transitive.rec (λu, u) C
end is_transitive
@ -66,13 +66,13 @@ is_equivalence_mk : is_reflexive R → is_symmetric R → is_transitive R → is
namespace is_equivalence
theorem is_reflexive {T : Type} (R : T → T → Type) {C : is_equivalence R} : is_reflexive R :=
is_equivalence_rec (λx y z, x) C
is_equivalence.rec (λx y z, x) C
theorem is_symmetric {T : Type} {R : T → T → Type} {C : is_equivalence R} : is_symmetric R :=
is_equivalence_rec (λx y z, y) C
is_equivalence.rec (λx y z, y) C
theorem is_transitive {T : Type} {R : T → T → Type} {C : is_equivalence R} : is_transitive R :=
is_equivalence_rec (λx y z, z) C
is_equivalence.rec (λx y z, z) C
end is_equivalence
@ -88,10 +88,10 @@ is_PER_mk : is_symmetric R → is_transitive R → is_PER R
namespace is_PER
theorem is_symmetric {T : Type} {R : T → T → Type} {C : is_PER R} : is_symmetric R :=
is_PER_rec (λx y, x) C
is_PER.rec (λx y, x) C
theorem is_transitive {T : Type} {R : T → T → Type} {C : is_PER R} : is_transitive R :=
is_PER_rec (λx y, y) C
is_PER.rec (λx y, y) C
end is_PER
@ -116,17 +116,17 @@ namespace congruence
abbreviation app {T1 : Type} {R1 : T1 → T1 → Prop} {T2 : Type} {R2 : T2 → T2 → Prop}
{f : T1 → T2} (C : congruence R1 R2 f) ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) :=
congruence_rec (λu, u) C x y
congruence.rec (λu, u) C x y
theorem infer {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
(f : T1 → T2) {C : congruence R1 R2 f} ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) :=
congruence_rec (λu, u) C x y
congruence.rec (λu, u) C x y
abbreviation app2 {T1 : Type} {R1 : T1 → T1 → Prop} {T2 : Type} {R2 : T2 → T2 → Prop}
{T3 : Type} {R3 : T3 → T3 → Prop}
{f : T1 → T2 → T3} (C : congruence2 R1 R2 R3 f) ⦃x1 y1 : T1⦄ ⦃x2 y2 : T2⦄ :
R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2) :=
congruence2_rec (λu, u) C x1 y1 x2 y2
congruence2.rec (λu, u) C x1 y1 x2 y2
-- ### general tools to build instances
@ -179,10 +179,10 @@ mp_like_mk {} : (a → b) → @mp_like R a b H
namespace mp_like
definition app {R : Type → Type → Prop} {a : Type} {b : Type} {H : R a b}
(C : mp_like H) : a → b := mp_like_rec (λx, x) C
(C : mp_like H) : a → b := mp_like.rec (λx, x) C
definition infer ⦃R : Type → Type → Prop⦄ {a : Type} {b : Type} (H : R a b)
{C : mp_like H} : a → b := mp_like_rec (λx, x) C
{C : mp_like H} : a → b := mp_like.rec (λx, x) C
end mp_like

7
src/frontends/lean/inductive_cmd.cpp
View file

@ -17,6 +17,7 @@ Author: Leonardo de Moura
#include "library/locals.h"
#include "library/placeholder.h"
#include "library/aliases.h"
#include "library/protected.h"
#include "library/explicit.h"
#include "library/opaque_hints.h"
#include "frontends/lean/decl_cmds.h"
@ -92,7 +93,7 @@ struct inductive_cmd_fn {
[[ noreturn ]] void throw_error(sstream const & strm) { throw parser_error(strm, m_pos); }
name mk_rec_name(name const & n) {
return n.append_after("_rec");
return n + name("rec");
}
/** \brief Parse the name of an inductive datatype or introduction rule,
@ -529,7 +530,9 @@ struct inductive_cmd_fn {
name d_name = inductive_decl_name(d);
name d_short_name(d_name.get_string());
env = create_alias(env, d_name, section_levels, section_params);
env = create_alias(env, mk_rec_name(d_name), section_levels, section_params);
name rec_name = mk_rec_name(d_name);
env = create_alias(env, rec_name, section_levels, section_params);
env = add_protected(env, rec_name);
for (intro_rule const & ir : inductive_decl_intros(d)) {
name ir_name = intro_rule_name(ir);
env = create_alias(env, ir_name, section_levels, section_params);

2
src/kernel/inductive/inductive.cpp
View file

@ -600,7 +600,7 @@ struct add_inductive_fn {
}
/** \brief Return the name of the eliminator/recursor for \c d. */
name get_elim_name(inductive_decl const & d) { return inductive_decl_name(d).append_after("_rec"); }
name get_elim_name(inductive_decl const & d) { return inductive_decl_name(d) + name("rec"); }
name get_elim_name(unsigned d_idx) { return get_elim_name(get_ith(m_decls, d_idx)); }

2
tests/lean/interactive/t4.input.expected.out
View file

@ -15,7 +15,7 @@ epsilon
Type
-- ACK
-- IDENTIFIER|6|21
nat.nat
nat
-- ACK
-- TYPE|6|26
Prop

22
tests/lean/run/algebra1.lean
View file

@ -23,12 +23,12 @@ namespace algebra
mk_add_struct : (A → A → A) → add_struct A
definition mul [inline] {A : Type} {s : mul_struct A} (a b : A)
:= mul_struct_rec (fun f, f) s a b
:= mul_struct.rec (fun f, f) s a b
infixl `*`:75 := mul
definition add [inline] {A : Type} {s : add_struct A} (a b : A)
:= add_struct_rec (fun f, f) s a b
:= add_struct.rec (fun f, f) s a b
infixl `+`:65 := add
end algebra
@ -49,7 +49,7 @@ namespace nat
definition to_nat (n : num) : nat
:= #algebra
num_rec zero (λ n, pos_num_rec (succ zero) (λ n r, r + r) (λ n r, r + r + succ zero) n) n
num.num.rec zero (λ n, num.pos_num.rec (succ zero) (λ n r, r + r) (λ n r, r + r + succ zero) n) n
end nat
namespace algebra
@ -58,10 +58,10 @@ namespace semigroup
mk_semigroup_struct : Π (mul : A → A → A), is_assoc mul → semigroup_struct A
definition mul [inline] {A : Type} (s : semigroup_struct A) (a b : A)
:= semigroup_struct_rec (fun f h, f) s a b
:= semigroup_struct.rec (fun f h, f) s a b
definition assoc [inline] {A : Type} (s : semigroup_struct A) : is_assoc (mul s)
:= semigroup_struct_rec (fun f h, h) s
:= semigroup_struct.rec (fun f h, h) s
definition is_mul_struct [inline] [instance] (A : Type) (s : semigroup_struct A) : mul_struct A
:= mk_mul_struct (mul s)
@ -70,10 +70,10 @@ namespace semigroup
mk_semigroup : Π (A : Type), semigroup_struct A → semigroup
definition carrier [inline] [coercion] (g : semigroup)
:= semigroup_rec (fun c s, c) g
:= semigroup.rec (fun c s, c) g
definition is_semigroup [inline] [instance] (g : semigroup) : semigroup_struct (carrier g)
:= semigroup_rec (fun c s, s) g
:= semigroup.rec (fun c s, s) g
end semigroup
namespace monoid
@ -83,10 +83,10 @@ namespace monoid
mk_monoid_struct : Π (mul : A → A → A) (id : A), is_assoc mul → is_id mul id → monoid_struct A
definition mul [inline] {A : Type} (s : monoid_struct A) (a b : A)
:= monoid_struct_rec (fun mul id a i, mul) s a b
:= monoid_struct.rec (fun mul id a i, mul) s a b
definition assoc [inline] {A : Type} (s : monoid_struct A) : is_assoc (mul s)
:= monoid_struct_rec (fun mul id a i, a) s
:= monoid_struct.rec (fun mul id a i, a) s
open semigroup
definition is_semigroup_struct [inline] [instance] (A : Type) (s : monoid_struct A) : semigroup_struct A
@ -96,10 +96,10 @@ namespace monoid
mk_monoid : Π (A : Type), monoid_struct A → monoid
definition carrier [inline] [coercion] (m : monoid)
:= monoid_rec (fun c s, c) m
:= monoid.rec (fun c s, c) m
definition is_monoid [inline] [instance] (m : monoid) : monoid_struct (carrier m)
:= monoid_rec (fun c s, s) m
:= monoid.rec (fun c s, s) m
end monoid
end algebra

8
tests/lean/run/class4.lean
View file

@ -5,7 +5,7 @@ zero : nat,
succ : nat → nat
definition add (x y : nat)
:= nat_rec x (λ n r, succ r) y
:= nat.rec x (λ n r, succ r) y
infixl `+`:65 := add
@ -16,7 +16,7 @@ theorem add_succ_left (x y : nat) : x + (succ y) = succ (x + y)
:= refl _
definition is_zero (x : nat)
:= nat_rec true (λ n r, false) x
:= nat.rec true (λ n r, false) x
theorem is_zero_zero : is_zero zero
:= eq_true_elim (refl _)
@ -25,7 +25,7 @@ theorem not_is_zero_succ (x : nat) : ¬ is_zero (succ x)
:= eq_false_elim (refl _)
theorem dichotomy (m : nat) : m = zero ∨ (∃ n, m = succ n)
:= nat_rec
:= nat.rec
(or_intro_left _ (refl zero))
(λ m H, or_intro_right _ (exists_intro m (refl (succ m))))
m
@ -57,7 +57,7 @@ inductive not_zero (x : nat) : Prop :=
not_zero_intro : ¬ is_zero x → not_zero x
theorem not_zero_not_is_zero {x : nat} (H : not_zero x) : ¬ is_zero x
:= not_zero_rec (λ H1, H1) H
:= not_zero.rec (λ H1, H1) H
theorem not_zero_add_right [instance] (x y : nat) (H : not_zero y) : not_zero (x + y)
:= not_zero_intro (not_zero_add x y (not_zero_not_is_zero H))

2
tests/lean/run/class5.lean
View file

@ -5,7 +5,7 @@ namespace algebra
mk_mul_struct : (A → A → A) → mul_struct A
definition mul [inline] {A : Type} {s : mul_struct A} (a b : A)
:= mul_struct_rec (λ f, f) s a b
:= mul_struct.rec (λ f, f) s a b
infixl `*`:75 := mul
end algebra

2
tests/lean/run/class7.lean
View file

@ -10,7 +10,7 @@ theorem inh_bool [instance] : inh Prop
:= inh_intro true
theorem inh_fun [instance] {A B : Type} (H : inh B) : inh (A → B)
:= inh_rec (λ b, inh_intro (λ a : A, b)) H
:= inh.rec (λ b, inh_intro (λ a : A, b)) H
definition assump := eassumption; now

4
tests/lean/run/class8.lean
View file

@ -7,7 +7,7 @@ inh_intro : A -> inh A
instance inh_intro
theorem inh_elim {A : Type} {B : Prop} (H1 : inh A) (H2 : A → B) : B
:= inh_rec H2 H1
:= inh.rec H2 H1
theorem inh_exists [instance] {A : Type} {P : A → Prop} (H : ∃x, P x) : inh A
:= obtain w Hw, from H, inh_intro w
@ -16,7 +16,7 @@ theorem inh_bool [instance] : inh Prop
:= inh_intro true
theorem inh_fun [instance] {A B : Type} (H : inh B) : inh (A → B)
:= inh_rec (λb, inh_intro (λa : A, b)) H
:= inh.rec (λb, inh_intro (λa : A, b)) H
theorem pair_inh [instance] {A : Type} {B : Type} (H1 : inh A) (H2 : inh B) : inh (prod A B)
:= inh_elim H1 (λa, inh_elim H2 (λb, inh_intro (pair a b)))

2
tests/lean/run/class_coe.lean
View file

@ -10,7 +10,7 @@ inductive add_struct (A : Type) :=
mk : (A → A → A) → add_struct A
definition add {A : Type} {S : add_struct A} (a b : A) : A :=
add_struct_rec (λ m, m) S a b
add_struct.rec (λ m, m) S a b
infixl `+`:65 := add

2
tests/lean/run/cody1.lean
View file

@ -20,6 +20,6 @@ notation `δ` := delta.
theorem false_aux : ¬ (δ (i delta))
:= assume H : δ (i delta),
have H' : r (i delta) (i delta),
from eq_rec H (symm retract),
from eq.rec H (symm retract),
H H'.
end

6
tests/lean/run/coe2.lean
View file

@ -5,10 +5,10 @@ namespace setoid
mk_setoid: Π (A : Type), (A → A → Prop) → setoid
definition carrier (s : setoid)
:= setoid_rec (λ a eq, a) s
:= setoid.rec (λ a eq, a) s
definition eqv {s : setoid} : carrier s → carrier s → Prop
:= setoid_rec (λ a eqv, eqv) s
:= setoid.rec (λ a eqv, eqv) s
infix `≈`:50 := eqv
@ -17,4 +17,4 @@ namespace setoid
inductive morphism (s1 s2 : setoid) : Type :=
mk_morphism : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism s1 s2
end setoid
end setoid

6
tests/lean/run/coe3.lean
View file

@ -5,10 +5,10 @@ namespace setoid
mk_setoid: Π (A : Type), (A → A → Prop) → setoid
definition carrier (s : setoid)
:= setoid_rec (λ a eq, a) s
:= setoid.rec (λ a eq, a) s
definition eqv {s : setoid} : carrier s → carrier s → Prop
:= setoid_rec (λ a eqv, eqv) s
:= setoid.rec (λ a eqv, eqv) s
infix `≈`:50 := eqv
@ -27,4 +27,4 @@ namespace setoid
mk_morphism2 : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism2 s1 s2
check mk_morphism2
end setoid
end setoid

6
tests/lean/run/coe4.lean
View file

@ -10,10 +10,10 @@ namespace setoid
definition test : Type.{2} := setoid.{0}
definition carrier (s : setoid)
:= setoid_rec (λ a eq, a) s
:= setoid.rec (λ a eq, a) s
definition eqv {s : setoid} : carrier s → carrier s → Prop
:= setoid_rec (λ a eqv, eqv) s
:= setoid.rec (λ a eqv, eqv) s
infix `≈`:50 := eqv
@ -31,4 +31,4 @@ namespace setoid
check morphism2
check mk_morphism2
end setoid
end setoid

6
tests/lean/run/coe5.lean
View file

@ -10,10 +10,10 @@ namespace setoid
definition test : Type.{2} := setoid.{0}
definition carrier (s : setoid)
:= setoid_rec (λ a eq, a) s
:= setoid.rec (λ a eq, a) s
definition eqv {s : setoid} : carrier s → carrier s → Prop
:= setoid_rec (λ a eqv, eqv) s
:= setoid.rec (λ a eqv, eqv) s
infix `≈`:50 := eqv
@ -37,4 +37,4 @@ namespace setoid
check my_struct
definition tst2 : Type.{4} := my_struct.{1 2 1 2}
end setoid
end setoid

2
tests/lean/run/coercion_bug2.lean
View file

@ -5,6 +5,6 @@ inductive list (T : Type) : Type :=
nil {} : list T,
cons : T → list T → list T
definition length {T : Type} : list T → nat := list_rec 0 (fun x l m, succ m)
definition length {T : Type} : list T → nat := list.rec 0 (fun x l m, succ m)
theorem length_nil {T : Type} : length (@nil T) = 0
:= refl _

4
tests/lean/run/congr_imp_bug.lean
View file

@ -14,7 +14,7 @@ mk : (∀x y : T1, R1 x y → R2 (f x) (f y)) → struc R1 R2 f
abbreviation app {T1 : Type} {T2 : Type} {R1 : T1 → T1 → Prop} {R2 : T2 → T2 → Prop}
{f : T1 → T2} (C : struc R1 R2 f) {x y : T1} : R1 x y → R2 (f x) (f y) :=
struc_rec id C x y
struc.rec id C x y
inductive struc2 {T1 : Type} {T2 : Type} {T3 : Type} (R1 : T1 → T1 → Prop)
(R2 : T2 → T2 → Prop) (R3 : T3 → T3 → Prop) (f : T1 → T2 → T3) : Prop :=
@ -25,7 +25,7 @@ abbreviation app2 {T1 : Type} {T2 : Type} {T3 : Type} {R1 : T1 → T1 → Prop}
{R2 : T2 → T2 → Prop} {R3 : T3 → T3 → Prop} {f : T1 → T2 → T3}
(C : struc2 R1 R2 R3 f) {x1 y1 : T1} {x2 y2 : T2}
: R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2) :=
struc2_rec id C x1 y1 x2 y2
struc2.rec id C x1 y1 x2 y2
theorem compose21
{T2 : Type} {R2 : T2 → T2 → Prop}

4
tests/lean/run/e14.lean
View file

@ -21,10 +21,10 @@ check vcons zero vnil
variable n : nat
check vcons n vnil
check vector_rec
check vector.rec
definition vector_to_list {A : Type} {n : nat} (v : vector A n) : list A
:= vector_rec (@nil A) (fun (n : nat) (a : A) (v : vector A n) (l : list A), cons a l) v
:= vector.rec (@nil A) (fun (n : nat) (a : A) (v : vector A n) (l : list A), cons a l) v
coercion vector_to_list

4
tests/lean/run/e15.lean
View file

@ -21,7 +21,7 @@ check vcons zero vnil
variable n : nat
check vcons n vnil
check vector_rec
check vector.rec
definition vector_to_list {A : Type} {n : nat} (v : vector A n) : list A
:= vector_rec nil (fun (n : nat) (a : A) (v : vector A n) (l : list A), cons a l) v
:= vector.rec nil (fun (n : nat) (a : A) (v : vector A n) (l : list A), cons a l) v

4
tests/lean/run/e16.lean
View file

@ -21,7 +21,7 @@ check vcons zero vnil
variable n : nat
check vcons n vnil
check vector_rec
check vector.rec
definition vector_to_list {A : Type} {n : nat} (v : vector A n) : list A
:= vector_rec nil (fun n a v l, cons a l) v
:= vector.rec nil (fun n a v l, cons a l) v

4
tests/lean/run/elab_bug1.lean
View file

@ -23,7 +23,7 @@ mk : (∀x y : T1, R1 x y → R2 (f x) (f y)) → congruence R1 R2 f
-- to trigger class inference
theorem congr_app {T1 : Type} {T2 : Type} (R1 : T1 → T1 → Prop) (R2 : T2 → T2 → Prop)
(f : T1 → T2) {C : congruence R1 R2 f} {x y : T1} : R1 x y → R2 (f x) (f y) :=
congruence_rec id C x y
congruence.rec id C x y
-- General tools to build instances
@ -59,7 +59,7 @@ theorem congr_not [instance] (T : Type) (R : T → T → Prop) (f : T → Prop)
theorem subst_iff {T : Type} {R : T → T → Prop} {P : T → Prop} {C : congruence R iff P}
{a b : T} (H : R a b) (H1 : P a) : P b :=
-- iff_mp_left (congruence_rec id C a b H) H1
-- iff_mp_left (congruence.rec id C a b H) H1
iff_elim_left (@congr_app _ _ R iff P C a b H) H1
theorem test2 (a b c d e : Prop) (H1 : a ↔ b) (H2 : a ∨ c → ¬(d → a)) : b ∨ c → ¬(d → b) :=

10
tests/lean/run/export.lean
View file

@ -1,18 +1,18 @@
import data.nat
variables a b : nat.nat
variables a b : nat
namespace boo
export nat
export nat (rec add)
check a + b
check nat.add
check boo.add
check add
end boo
check boo.nat_rec
check boo.rec
open boo
check a + b
check boo.nat_rec
check nat_rec
check boo.rec
check nat.rec

6
tests/lean/run/group.lean
View file

@ -20,15 +20,15 @@ inductive group : Type :=
mk_group : Π (A : Type), group_struct A → group
definition carrier (g : group) : Type
:= group_rec (λ c s, c) g
:= group.rec (λ c s, c) g
definition group_to_struct [instance] (g : group) : group_struct (carrier g)
:= group_rec (λ (A : Type) (s : group_struct A), s) g
:= group.rec (λ (A : Type) (s : group_struct A), s) g
check group_struct
definition mul [inline] {A : Type} {s : group_struct A} (a b : A) : A
:= group_struct_rec (λ mul one inv h1 h2 h3, mul) s a b
:= group_struct.rec (λ mul one inv h1 h2 h3, mul) s a b
infixl `*`:75 := mul

6
tests/lean/run/group2.lean
View file

@ -20,17 +20,17 @@ inductive group : Type :=
mk_group : Π (A : Type), group_struct A → group
definition carrier (g : group) : Type
:= group_rec (λ c s, c) g
:= group.rec (λ c s, c) g
coercion carrier
definition group_to_struct [instance] (g : group) : group_struct (carrier g)
:= group_rec (λ (A : Type) (s : group_struct A), s) g
:= group.rec (λ (A : Type) (s : group_struct A), s) g
check group_struct
definition mul [inline] {A : Type} {s : group_struct A} (a b : A) : A
:= group_struct_rec (λ mul one inv h1 h2 h3, mul) s a b
:= group_struct.rec (λ mul one inv h1 h2 h3, mul) s a b
infixl `*`:75 := mul

2
tests/lean/run/ind0.lean
View file

@ -3,4 +3,4 @@ zero : nat,
succ : nat → nat
check nat
check nat_rec.{1}
check nat.rec.{1}

2
tests/lean/run/ind1.lean
View file

@ -4,4 +4,4 @@ cons : A → list A → list A
check list.{1}
check cons.{1}
check list_rec.{1 1}
check list.rec.{1 1}

2
tests/lean/run/ind2.lean
View file

@ -9,4 +9,4 @@ vcons : Π {n : nat}, A → vector A n → vector A (succ n)
check vector.{1}
check vnil.{1}
check vcons.{1}
check vector_rec.{1 1}
check vector.rec.{1 1}

6
tests/lean/run/ind3.lean
View file

@ -6,8 +6,8 @@ cons : tree A → forest A → forest A
check tree.{1}
check forest.{1}
check tree_rec.{1 1}
check forest_rec.{1 1}
check tree.rec.{1 1}
check forest.rec.{1 1}
print "==============="
@ -16,4 +16,4 @@ mk_group : Π (carrier : Type) (mul : carrier → carrier → carrier) (one : ca
check group.{1}
check group.{2}
check group_rec.{1 1}
check group.rec.{1 1}

2
tests/lean/run/ind5.lean
View file

@ -6,4 +6,4 @@ or_intro_right : B → or A B
check or
check or_intro_left
check or_rec
check or.rec

4
tests/lean/run/ind6.lean
View file

@ -6,5 +6,5 @@ cons : tree.{u} A → forest.{u} A → forest.{u} A
check tree.{1}
check forest.{1}
check tree_rec.{1 1}
check forest_rec.{1 1}
check tree.rec.{1 1}
check forest.rec.{1 1}

2
tests/lean/run/ind7.lean
View file

@ -5,7 +5,7 @@ namespace list
check list.{1}
check cons.{1}
check list_rec.{1 1}
check list.rec.{1 1}
end list
check list.list.{1}

2
tests/lean/run/is_nil.lean
View file

@ -6,7 +6,7 @@ nil {} : list A,
cons : A → list A → list A
definition is_nil {A : Type} (l : list A) : Prop
:= list_rec true (fun h t r, false) l
:= list.rec true (fun h t r, false) l
theorem is_nil_nil (A : Type) : is_nil (@nil A)
:= eq_true_elim (refl true)

4
tests/lean/run/list_elab1.lean
View file

@ -17,10 +17,10 @@ cons : T → list T → list T
theorem list_induction_on {T : Type} {P : list T → Prop} (l : list T) (Hnil : P nil)
(Hind : forall x : T, forall l : list T, forall H : P l, P (cons x l)) : P l :=
list_rec Hnil Hind l
list.rec Hnil Hind l
definition concat {T : Type} (s t : list T) : list T :=
list_rec t (fun x : T, fun l : list T, fun u : list T, cons x u) s
list.rec t (fun x : T, fun l : list T, fun u : list T, cons x u) s
theorem concat_nil {T : Type} (t : list T) : concat t nil = t :=
list_induction_on t (refl (concat nil nil))

2
tests/lean/run/match1.lean
View file

@ -23,6 +23,6 @@ end
local f = Const("f")
local two1 = Const("two1")
local two2 = Const("two2")
local succ = Const({"nat", "succ"})
local succ = Const({"succ"})
tst_match(f(succ(mk_var(0)), two1), f(two2, two2))
*)

6
tests/lean/run/matrix.lean
View file

@ -11,9 +11,9 @@ theorem same_dim_eq_args {A : Type} {m1 m2 m1' m2' : matrix A} (H1 : m1 = m1') (
subst H1 (subst H2 H)
theorem add_congr {A : Type} (m1 m2 m1' m2' : matrix A) (H1 : m1 = m1') (H2 : m2 = m2') (H : same_dim m1 m2) : @add A m1 m2 H = @add A m1' m2' (same_dim_eq_args H1 H2 H) :=
have base : ∀ (H1 : m1 = m1) (H2 : m2 = m2), @add A m1 m2 H = @add A m1 m2 (eq_rec (eq_rec H H1) H2), from
have base : ∀ (H1 : m1 = m1) (H2 : m2 = m2), @add A m1 m2 H = @add A m1 m2 (eq.rec (eq.rec H H1) H2), from
assume H1 H2, rfl,
have general : ∀ (H1 : m1 = m1') (H2 : m2 = m2'), @add A m1 m2 H = @add A m1' m2' (eq_rec (eq_rec H H1) H2), from
have general : ∀ (H1 : m1 = m1') (H2 : m2 = m2'), @add A m1 m2 H = @add A m1' m2' (eq.rec (eq.rec H H1) H2), from
subst H1 (subst H2 base),
calc @add A m1 m2 H = @add A m1' m2' (eq_rec (eq_rec H H1) H2) : general H1 H2
calc @add A m1 m2 H = @add A m1' m2' (eq.rec (eq.rec H H1) H2) : general H1 H2
... = @add A m1' m2' (same_dim_eq_args H1 H2 H) : same_dim_irrel

4
tests/lean/run/matrix2.lean
View file

@ -8,8 +8,8 @@ theorem same_dim_eq_args {A : Type} {m1 m2 m1' m2' : matrix A} (H1 : m1 = m1') (
subst H1 (subst H2 H)
theorem add_congr {A : Type} (m1 m2 m1' m2' : matrix A) (H1 : m1 = m1') (H2 : m2 = m2') (H : same_dim m1 m2) : @add A m1 m2 H = @add A m1' m2' (same_dim_eq_args H1 H2 H) :=
have base : ∀ (H1 : m1 = m1) (H2 : m2 = m2), @add A m1 m2 H = @add A m1 m2 (eq_rec (eq_rec H H1) H2), from
have base : ∀ (H1 : m1 = m1) (H2 : m2 = m2), @add A m1 m2 H = @add A m1 m2 (eq.rec (eq.rec H H1) H2), from
assume H1 H2, rfl,
have general : ∀ (H1 : m1 = m1') (H2 : m2 = m2'), @add A m1 m2 H = @add A m1' m2' (eq_rec (eq_rec H H1) H2), from
have general : ∀ (H1 : m1 = m1') (H2 : m2 = m2'), @add A m1 m2 H = @add A m1' m2' (eq.rec (eq.rec H H1) H2), from
subst H1 (subst H2 base),
general H1 H2

4
tests/lean/run/nat_bug.lean
View file

@ -6,9 +6,9 @@ zero : nat,
succ : nat → nat
theorem induction_on {P : nat → Prop} (a : nat) (H1 : P zero) (H2 : ∀ (n : nat) (IH : P n), P (succ n)) : P a
:= nat_rec H1 H2 a
:= nat.rec H1 H2 a
definition pred (n : nat) := nat_rec zero (fun m x, m) n
definition pred (n : nat) := nat.rec zero (fun m x, m) n
theorem pred_zero : pred zero = zero := refl _
theorem pred_succ (n : nat) : pred (succ n) = n := refl _

4
tests/lean/run/nat_bug2.lean
View file

@ -6,9 +6,9 @@ zero : nat,
succ : nat → nat
abbreviation plus (x y : nat) : nat
:= nat_rec x (λn r, succ r) y
:= nat.rec x (λn r, succ r) y
definition to_nat [coercion] [inline] (n : num) : nat
:= num_rec zero (λn, pos_num_rec (succ zero) (λn r, plus r (plus r (succ zero))) (λn r, plus r r) n) n
:= num.num.rec zero (λn, num.pos_num.rec (succ zero) (λn r, plus r (plus r (succ zero))) (λn r, plus r r) n) n
definition add (x y : nat) : nat
:= plus x y
variable le : nat → nat → Prop

4
tests/lean/run/nat_bug3.lean
View file

@ -6,9 +6,9 @@ zero : nat,
succ : nat → nat
abbreviation plus (x y : nat) : nat
:= nat_rec x (λn r, succ r) y
:= nat.rec x (λn r, succ r) y
definition to_nat [coercion] [inline] (n : num) : nat
:= num_rec zero (λn, pos_num_rec (succ zero) (λn r, plus r (plus r (succ zero))) (λn r, plus r r) n) n
:= num.num.rec zero (λn, num.pos_num.rec (succ zero) (λn r, plus r (plus r (succ zero))) (λn r, plus r r) n) n
definition add (x y : nat) : nat
:= plus x y
variable le : nat → nat → Prop

4
tests/lean/run/nat_bug4.lean
View file

@ -5,9 +5,9 @@ inductive nat : Type :=
zero : nat,
succ : nat → nat
definition add (x y : nat) : nat := nat_rec x (λn r, succ r) y
definition add (x y : nat) : nat := nat.rec x (λn r, succ r) y
infixl `+`:65 := add
definition mul (n m : nat) := nat_rec zero (fun m x, x + n) m
definition mul (n m : nat) := nat.rec zero (fun m x, x + n) m
infixl `*`:75 := mul
axiom mul_succ_right (n m : nat) : n * succ m = n * m + n

4
tests/lean/run/nat_bug5.lean
View file

@ -5,9 +5,9 @@ inductive nat : Type :=
zero : nat,
succ : nat → nat
definition add (x y : nat) : nat := nat_rec x (λn r, succ r) y
definition add (x y : nat) : nat := nat.rec x (λn r, succ r) y
infixl `+`:65 := add
definition mul (n m : nat) := nat_rec zero (fun m x, x + n) m
definition mul (n m : nat) := nat.rec zero (fun m x, x + n) m
infixl `*`:75 := mul
axiom add_one (n:nat) : n + (succ zero) = succ n

4
tests/lean/run/nat_bug6.lean
View file

@ -5,9 +5,9 @@ inductive nat : Type :=
zero : nat,
succ : nat → nat
definition add (x y : nat) : nat := nat_rec x (λn r, succ r) y
definition add (x y : nat) : nat := nat.rec x (λn r, succ r) y
infixl `+`:65 := add
definition mul (n m : nat) := nat_rec zero (fun m x, x + n) m
definition mul (n m : nat) := nat.rec zero (fun m x, x + n) m
infixl `*`:75 := mul
axiom mul_zero_right (n : nat) : n * zero = zero

2
tests/lean/run/nat_bug7.lean
View file

@ -4,7 +4,7 @@ inductive nat : Type :=
zero : nat,
succ : nat → nat
definition add (x y : nat) : nat := nat_rec x (λn r, succ r) y
definition add (x y : nat) : nat := nat.rec x (λn r, succ r) y
infixl `+`:65 := add
axiom add_right_comm (n m k : nat) : n + m + k = n + k + m

4
tests/lean/run/opaque_hint_bug.lean
View file

@ -7,8 +7,8 @@ section
variable {T : Type}
definition concat (s t : list T) : list T
:= list_rec t (fun x l u, cons x u) s
:= list.rec t (fun x l u, cons x u) s
opaque_hint (hiding concat)
end
end

6
tests/lean/run/rel.lean
View file

@ -7,13 +7,13 @@ namespace is_equivalence
mk : is_reflexive R → is_symmetric R → is_transitive R → cls R
theorem is_reflexive {T : Type} {R : T → T → Type} {C : cls R} : is_reflexive R :=
cls_rec (λx y z, x) C
cls.rec (λx y z, x) C
theorem is_symmetric {T : Type} {R : T → T → Type} {C : cls R} : is_symmetric R :=
cls_rec (λx y z, y) C
cls.rec (λx y z, y) C
theorem is_transitive {T : Type} {R : T → T → Type} {C : cls R} : is_transitive R :=
cls_rec (λx y z, z) C
cls.rec (λx y z, z) C
end is_equivalence

4
tests/lean/run/sum_bug.lean
View file

@ -17,7 +17,7 @@ infixr `+`:25 := sum
abbreviation rec_on {A B : Type} {C : (A + B) → Type} (s : A + B)
(H1 : ∀a : A, C (inl B a)) (H2 : ∀b : B, C (inr A b)) : C s :=
sum_rec H1 H2 s
sum.rec H1 H2 s
theorem inl_inj {A B : Type} {a1 a2 : A} (H : inl B a1 = inl B a2) : a1 = a2 :=
@ -28,7 +28,7 @@ H2
abbreviation cases_on {A B : Type} {P : (A + B) → Prop} (s : A + B)
(H1 : ∀a : A, P (inl B a)) (H2 : ∀b : B, P (inr A b)) : P s :=
sum_rec H1 H2 s
sum.rec H1 H2 s
theorem inl_neq_inr {A B : Type} {a : A} {b : B} (H : inl B a = inr A b) : false :=
let f := λs, rec_on s (λa', a = a') (λb, false) in

10
tests/lean/run/tactic23.lean
View file

@ -1,5 +1,5 @@
import logic
open num (num pos_num num_rec pos_num_rec)
open num (num pos_num num.rec pos_num.rec)
open tactic
inductive nat : Type :=
@ -7,7 +7,7 @@ zero : nat,
succ : nat → nat
definition add [inline] (a b : nat) : nat
:= nat_rec a (λ n r, succ r) b
:= nat.rec a (λ n r, succ r) b
infixl `+`:65 := add
definition one [inline] := succ zero
@ -15,9 +15,9 @@ definition one [inline] := succ zero
-- Define coercion from num -> nat
-- By default the parser converts numerals into a binary representation num
definition pos_num_to_nat [inline] (n : pos_num) : nat
:= pos_num_rec one (λ n r, r + r) (λ n r, r + r + one) n
:= pos_num.rec one (λ n r, r + r) (λ n r, r + r + one) n
definition num_to_nat [inline] (n : num) : nat
:= num_rec zero (λ n, pos_num_to_nat n) n
:= num.rec zero (λ n, pos_num_to_nat n) n
coercion num_to_nat
-- Now we can write 2 + 3, the coercion will be applied
@ -30,7 +30,7 @@ theorem T1 {p : nat → Prop} {a : nat } (H : p (a+2)) : ∃ x, p (succ x)
:= by apply exists_intro; assump
definition is_zero (n : nat)
:= nat_rec true (λ n r, false) n
:= nat.rec true (λ n r, false) n
theorem T2 : ∃ a, (is_zero a) = true
:= by apply exists_intro; apply refl

3
tests/lean/run/tactic26.lean
View file

@ -1,6 +1,7 @@
import logic
open tactic inhabited
namespace foo
inductive sum (A : Type) (B : Type) : Type :=
inl : A → sum A B,
inr : B → sum A B
@ -19,3 +20,5 @@ definition my_tac := fixpoint (λ t, [ apply @inl_inhabited; t
tactic_hint [inhabited] my_tac
theorem T : inhabited (sum false num.num)
end foo

3
tests/lean/run/tactic28.lean
View file

@ -1,6 +1,7 @@
import logic
open tactic inhabited
namespace foo
inductive sum (A : Type) (B : Type) : Type :=
inl : A → sum A B,
inr : B → sum A B
@ -22,3 +23,5 @@ definition my_tac := repeat (trace "iteration"; state;
tactic_hint [inhabited] my_tac
theorem T : inhabited (sum false num.num)
end foo

7
tests/lean/run/trans.lean
View file

@ -4,7 +4,7 @@
import logic
definition transport {A : Type} {a b : A} {P : A → Type} (p : a = b) (H : P a) : P b
:= eq_rec H p
:= eq.rec H p
theorem transport_refl {A : Type} {a : A} {P : A → Type} (H : P a) : transport (refl a) H = H
:= refl H
@ -20,12 +20,11 @@ theorem transport_eq {A : Type} {a : A} {P : A → Type} (p : a = a) (H : P a) :
theorem dcongr {A : Type} {B : A → Type} {a b : A} (f : Π x, B x) (p : a = b) : transport p (f a) = f b
:= have H1 : ∀ p1 : a = a, transport p1 (f a) = f a, from
assume p1 : a = a, transport_eq p1 (f a),
eq_rec H1 p p
eq.rec H1 p p
theorem transport_trans {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p, transport p1 (transport p H) = transport (trans p1 p) H, from
take p, calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2
eq.rec H1 p2 p2

6
tests/lean/run/uni.lean
View file

@ -4,11 +4,11 @@ inductive nat : Type :=
zero : nat,
succ : nat → nat
check @nat_rec
check @nat.rec
(*
local env = get_env()
local nat_rec = Const("nat_rec", {1})
local nat_rec = Const({"nat", "rec"}, {1})
local nat = Const("nat")
local n = Local("n", nat)
local C = Fun(n, Prop)
@ -45,4 +45,4 @@ end
test_unify(env, t(m), tt, 1)
test_unify(env, t(m), ff, 1)
*)
*)

6
tests/lean/run/uni2.lean
View file

@ -6,11 +6,11 @@ succ : nat → nat
variable f : nat → nat
check @nat_rec
check @nat.rec
(*
local env = get_env()
local nat_rec = Const("nat_rec", {1})
local nat_rec = Const({"nat", "rec"}, {1})
local nat = Const("nat")
local f = Const("f")
local n = Local("n", nat)
@ -47,4 +47,4 @@ function test_unify(env, lhs, rhs, num_s)
end
test_unify(env, f(t(m)), f(tt), 1)
*)
*)

2
tests/lean/run/uni_issue1.lean
View file

@ -5,4 +5,4 @@ zero : nat,
succ : nat → nat
definition is_zero (n : nat)
:= nat_rec true (λ n r, false) n
:= nat.rec true (λ n r, false) n

4
tests/lean/run/univ_bug1.lean
View file

@ -16,10 +16,10 @@ inductive simplifies_to {T : Type} (t1 t2 : T) : Prop :=
mk : t1 = t2 → simplifies_to t1 t2
theorem get_eq {T : Type} {t1 t2 : T} (C : simplifies_to t1 t2) : t1 = t2 :=
simplifies_to_rec (λx, x) C
simplifies_to.rec (λx, x) C
theorem infer_eq {T : Type} (t1 t2 : T) {C : simplifies_to t1 t2} : t1 = t2 :=
simplifies_to_rec (λx, x) C
simplifies_to.rec (λx, x) C
theorem simp_app [instance] (S T : Type) (f1 f2 : S → T) (s1 s2 : S)
(C1 : simplifies_to f1 f2) (C2 : simplifies_to s1 s2) : simplifies_to (f1 s1) (f2 s2) :=

4
tests/lean/run/univ_bug2.lean
View file

@ -13,10 +13,10 @@ inductive simplifies_to {T : Type} (t1 t2 : T) : Prop :=
mk : t1 = t2 → simplifies_to t1 t2
theorem get_eq {T : Type} {t1 t2 : T} (C : simplifies_to t1 t2) : t1 = t2 :=
simplifies_to_rec (λx, x) C
simplifies_to.rec (λx, x) C
theorem infer_eq {T : Type} (t1 t2 : T) {C : simplifies_to t1 t2} : t1 = t2 :=
simplifies_to_rec (λx, x) C
simplifies_to.rec (λx, x) C
theorem simp_app [instance] (S : Type) (T : Type) (f1 f2 : S → T) (s1 s2 : S)
(C1 : simplifies_to f1 f2) (C2 : simplifies_to s1 s2) : simplifies_to (f1 s1) (f2 s2) :=

28
tests/lean/run/uuu.lean
View file

@ -26,15 +26,15 @@ inductive total2 {T: Type} (P: T → Type) : Type :=
tpair : Π (t : T) (tp : P t), total2 P
definition pr1 {T : Type} {P : T → Type} (tp : total2 P) : T
:= total2_rec (λ a b, a) tp
:= total2.rec (λ a b, a) tp
definition pr2 {T : Type} {P : T → Type} (tp : total2 P) : P (pr1 tp)
:= total2_rec (λ a b, b) tp
:= total2.rec (λ a b, b) tp
inductive Phant (T : Type) : Type :=
phant : Phant T
definition fromempty {X : Type} : empty → X
:= λe, empty_rec (λe, X) e
:= λe, empty.rec (λe, X) e
definition tounit {X : Type} : X → unit
:= λx, tt
@ -50,7 +50,7 @@ abbreviation funcomp {X : Type} {Y : Type} {Z : Type} (f : X → Y) (g : Y → Z
infixl `∘`:60 := funcomp
definition iteration {T : Type} (f : T → T) (n : nat) : T → T
:= nat_rec (idfun T) (λ m fm, funcomp fm f) n
:= nat.rec (idfun T) (λ m fm, funcomp fm f) n
definition adjev {X : Type} {Y : Type} (x : X) (f : X → Y) := f x
@ -98,16 +98,16 @@ definition logeqnegs {X : Type} {Y : Type} (l : X ↔ Y) : (neg X) ↔ (neg Y)
infix `=`:50 := paths
definition pathscomp0 {X : Type} {a b c : X} (e1 : a = b) (e2 : b = c) : a = c
:= paths_rec e1 e2
:= paths.rec e1 e2
definition pathscomp0rid {X : Type} {a b : X} (e1 : a = b) : pathscomp0 e1 (idpath b) = e1
:= idpath _
definition pathsinv0 {X : Type} {a b : X} (e : a = b) : b = a
:= paths_rec (idpath _) e
:= paths.rec (idpath _) e
definition transport {A : Type} {a b : A} {P : A → Type} (H1 : a = b) (H2 : P a) : P b
:= paths_rec H2 H1
:= paths.rec H2 H1
infixr `▸`:75 := transport
infixr `⬝`:75 := pathscomp0
@ -120,13 +120,13 @@ definition idtrans {A : Type} (x : A) : (idpath x) ⬝ (idpath x) = (idpath x)
:= idpath (idpath x)
definition pathsinv0l {X : Type} {a b : X} (e : a = b) : e⁻¹ ⬝ e = idpath b
:= paths_rec (idinv a⁻¹ ▸ idtrans a) e
:= paths.rec (idinv a⁻¹ ▸ idtrans a) e
definition pathsinv0r {A : Type} {x y : A} (p : x = y) : p⁻¹ ⬝ p = idpath y
:= paths_rec (idinv x⁻¹ ▸ idtrans x) p
:= paths.rec (idinv x⁻¹ ▸ idtrans x) p
definition pathsinv0inv0 {A : Type} {x y : A} (p : x = y) : (p⁻¹)⁻¹ = p
:= paths_rec (idpath (idpath x)) p
:= paths.rec (idpath (idpath x)) p
definition pathsdirprod {X : Type} {Y : Type} {x1 x2 : X} {y1 y2 : Y} (ex : x1 = x2) (ey : y1 = y2 ) : dirprodpair x1 y1 = dirprodpair x2 y2
:= ex ▸ ey ▸ idpath (dirprodpair x1 y1)
@ -137,13 +137,13 @@ definition maponpaths {T1 : Type} {T2 : Type} (f : T1 → T2) {t1 t2 : T1} (e :
definition ap {T1 : Type} {T2 : Type} := @maponpaths T1 T2
definition maponpathscomp0 {X : Type} {Y : Type} {x y z : X} (f : X → Y) (p : x = y) (q : y = z) : ap f (p ⬝ q) = (ap f p) ⬝ (ap f q)
:= paths_rec (idpath _) q
:= paths.rec (idpath _) q
definition maponpathsinv0 {X : Type} {Y : Type} (f : X → Y) {x1 x2 : X} (e : x1 = x2 ) : ap f (e⁻¹) = (ap f e)⁻¹
:= paths_rec (idpath _) e
:= paths.rec (idpath _) e
lemma maponpathsidfun {X : Type} {x x' : X} (e : x = x') : ap (idfun X) e = e
:= paths_rec (idpath _) e
:= paths.rec (idpath _) e
lemma maponpathscomp {X : Type} {Y : Type} {Z : Type} {x x' : X} (f : X → Y) (g : Y → Z) (e : x = x') : ap g (ap f e) = ap (f ∘ g) e
:= paths_rec (idpath _) e
:= paths.rec (idpath _) e

10
tests/lean/slow/list_elab2.lean
View file

@ -33,7 +33,7 @@ variable {T : Type}
theorem list_induction_on {P : list T → Prop} (l : list T) (Hnil : P nil)
(Hind : forall x : T, forall l : list T, forall H : P l, P (cons x l)) : P l :=
list_rec Hnil Hind l
list.rec Hnil Hind l
theorem list_cases_on {P : list T → Prop} (l : list T) (Hnil : P nil)
(Hcons : forall x : T, forall l : list T, P (cons x l)) : P l :=
@ -46,7 +46,7 @@ notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l
-- ------
definition concat (s t : list T) : list T :=
list_rec t (fun x : T, fun l : list T, fun u : list T, cons x u) s
list.rec t (fun x : T, fun l : list T, fun u : list T, cons x u) s
infixl `++` : 65 := concat
@ -97,7 +97,7 @@ list_induction_on s (refl _)
-- Length
-- ------
definition length : list T → ℕ := list_rec 0 (fun x l m, succ m)
definition length : list T → ℕ := list.rec 0 (fun x l m, succ m)
-- TODO: cannot replace zero by 0
theorem length_nil : length (@nil T) = zero := refl _
@ -121,7 +121,7 @@ list_induction_on s
-- Reverse
-- -------
definition reverse : list T → list T := list_rec nil (fun x l r, r ++ [x])
definition reverse : list T → list T := list.rec nil (fun x l r, r ++ [x])
theorem reverse_nil : reverse (@nil T) = nil := refl _
@ -159,7 +159,7 @@ list_induction_on l (refl _)
-- TODO: define reverse from append
definition append (x : T) : list T → list T := list_rec (x :: nil) (fun y l l', y :: l')
definition append (x : T) : list T → list T := list.rec (x :: nil) (fun y l l', y :: l')
theorem append_nil (x : T) : append x nil = [x] := refl _

6
tests/lean/slow/nat_bug1.lean
View file

@ -13,11 +13,11 @@ succ : nat → nat
notation `ℕ`:max := nat
abbreviation plus (x y : ℕ) : ℕ
:= nat_rec x (λ n r, succ r) y
:= nat.rec x (λ n r, succ r) y
definition to_nat [coercion] [inline] (n : num) : ℕ
:= num_rec zero (λ n, pos_num_rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n
:= num.num.rec zero (λ n, num.pos_num.rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n
print "=================="
theorem nat_rec_zero {P : ℕ → Type} (x : P 0) (f : ∀m, P m → P (succ m)) : nat_rec x f 0 = x :=
theorem nat_rec_zero {P : ℕ → Type} (x : P 0) (f : ∀m, P m → P (succ m)) : nat.rec x f 0 = x :=
refl _

22
tests/lean/slow/nat_bug2.lean
View file

@ -15,10 +15,10 @@ succ : nat → nat
notation `ℕ`:max := nat
abbreviation plus (x y : ℕ) : ℕ
:= nat_rec x (λ n r, succ r) y
:= nat.rec x (λ n r, succ r) y
definition to_nat [coercion] [inline] (n : num) : ℕ
:= num_rec zero (λ n, pos_num_rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n
:= num.num.rec zero (λ n, num.pos_num.rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n
namespace helper_tactics
definition apply_refl := apply @refl
@ -26,28 +26,28 @@ namespace helper_tactics
end helper_tactics
open helper_tactics
theorem nat_rec_zero {P : ℕ → Type} (x : P 0) (f : ∀m, P m → P (succ m)) : nat_rec x f 0 = x
theorem nat_rec_zero {P : ℕ → Type} (x : P 0) (f : ∀m, P m → P (succ m)) : nat.rec x f 0 = x
theorem nat_rec_succ {P : ℕ → Type} (x : P 0) (f : ∀m, P m → P (succ m)) (n : ℕ) : nat_rec x f (succ n) = f n (nat_rec x f n)
theorem nat_rec_succ {P : ℕ → Type} (x : P 0) (f : ∀m, P m → P (succ m)) (n : ℕ) : nat.rec x f (succ n) = f n (nat.rec x f n)
theorem induction_on {P : ℕ → Prop} (a : ℕ) (H1 : P 0) (H2 : ∀ (n : ℕ) (IH : P n), P (succ n)) : P a
:= nat_rec H1 H2 a
:= nat.rec H1 H2 a
definition rec_on {P : ℕ → Type} (n : ℕ) (H1 : P 0) (H2 : ∀m, P m → P (succ m)) : P n
:= nat_rec H1 H2 n
:= nat.rec H1 H2 n
-------------------------------------------------- succ pred
theorem succ_ne_zero (n : ℕ) : succ n ≠ 0
:= assume H : succ n = 0,
have H2 : true = false, from
let f := (nat_rec false (fun a b, true)) in
let f := (nat.rec false (fun a b, true)) in
calc true = f (succ n) : _
... = f 0 : {H}
... = false : _,
absurd H2 true_ne_false
definition pred (n : ℕ) := nat_rec 0 (fun m x, m) n
definition pred (n : ℕ) := nat.rec 0 (fun m x, m) n
theorem pred_zero : pred 0 = 0
@ -260,11 +260,11 @@ theorem add_one_left (n:ℕ) : 1 + n = succ n
--the following theorem has a terrible name, but since the name is not a substring or superstring of another name, it is at least easy to globally replace it
theorem induction_plus_one {P : ℕ → Prop} (a : ℕ) (H1 : P 0)
(H2 : ∀ (n : ℕ) (IH : P n), P (n + 1)) : P a
:= nat_rec H1 (take n IH, (add_one n) ▸ (H2 n IH)) a
:= nat.rec H1 (take n IH, (add_one n) ▸ (H2 n IH)) a
-------------------------------------------------- mul
definition mul (n m : ℕ) := nat_rec 0 (fun m x, x + n) m
definition mul (n m : ℕ) := nat.rec 0 (fun m x, x + n) m
infixl `*`:75 := mul
theorem mul_zero_right (n:ℕ) : n * 0 = 0
@ -1061,7 +1061,7 @@ theorem mul_eq_one {n m : ℕ} (H : n * m = 1) : n = 1 ∧ m = 1
-------------------------------------------------- sub
definition sub (n m : ℕ) : ℕ := nat_rec n (fun m x, pred x) m
definition sub (n m : ℕ) : ℕ := nat.rec n (fun m x, pred x) m
infixl `-`:65 := sub
theorem sub_zero_right (n : ℕ) : n - 0 = n
theorem sub_succ_right (n m : ℕ) : n - succ m = pred (n - m)

22
tests/lean/slow/nat_wo_hints.lean
View file

@ -15,10 +15,10 @@ succ : nat → nat
notation `ℕ`:max := nat
abbreviation plus (x y : ℕ) : ℕ
:= nat_rec x (λ n r, succ r) y
:= nat.rec x (λ n r, succ r) y
definition to_nat [coercion] [inline] (n : num) : ℕ
:= num_rec zero (λ n, pos_num_rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n
:= num.num.rec zero (λ n, num.pos_num.rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n
namespace helper_tactics
definition apply_refl := apply @refl
@ -26,28 +26,28 @@ namespace helper_tactics
end helper_tactics
open helper_tactics
theorem nat_rec_zero {P : ℕ → Type} (x : P 0) (f : ∀m, P m → P (succ m)) : nat_rec x f 0 = x
theorem nat_rec_zero {P : ℕ → Type} (x : P 0) (f : ∀m, P m → P (succ m)) : nat.rec x f 0 = x
theorem nat_rec_succ {P : ℕ → Type} (x : P 0) (f : ∀m, P m → P (succ m)) (n : ℕ) : nat_rec x f (succ n) = f n (nat_rec x f n)
theorem nat_rec_succ {P : ℕ → Type} (x : P 0) (f : ∀m, P m → P (succ m)) (n : ℕ) : nat.rec x f (succ n) = f n (nat.rec x f n)
theorem induction_on {P : ℕ → Prop} (a : ℕ) (H1 : P 0) (H2 : ∀ (n : ℕ) (IH : P n), P (succ n)) : P a
:= nat_rec H1 H2 a
:= nat.rec H1 H2 a
definition rec_on {P : ℕ → Type} (n : ℕ) (H1 : P 0) (H2 : ∀m, P m → P (succ m)) : P n
:= nat_rec H1 H2 n
:= nat.rec H1 H2 n
-------------------------------------------------- succ pred
theorem succ_ne_zero (n : ℕ) : succ n ≠ 0
:= assume H : succ n = 0,
have H2 : true = false, from
let f := (nat_rec false (fun a b, true)) in
let f := (nat.rec false (fun a b, true)) in
calc true = f (succ n) : _
... = f 0 : {H}
... = false : _,
absurd H2 true_ne_false
definition pred (n : ℕ) := nat_rec 0 (fun m x, m) n
definition pred (n : ℕ) := nat.rec 0 (fun m x, m) n
theorem pred_zero : pred 0 = 0
@ -260,11 +260,11 @@ theorem add_one_left (n:ℕ) : 1 + n = succ n
--the following theorem has a terrible name, but since the name is not a substring or superstring of another name, it is at least easy to globally replace it
theorem induction_plus_one {P : ℕ → Prop} (a : ℕ) (H1 : P 0)
(H2 : ∀ (n : ℕ) (IH : P n), P (n + 1)) : P a
:= nat_rec H1 (take n IH, (add_one n) ▸ (H2 n IH)) a
:= nat.rec H1 (take n IH, (add_one n) ▸ (H2 n IH)) a
-------------------------------------------------- mul
definition mul (n m : ℕ) := nat_rec 0 (fun m x, x + n) m
definition mul (n m : ℕ) := nat.rec 0 (fun m x, x + n) m
infixl `*`:75 := mul
theorem mul_zero_right (n:ℕ) : n * 0 = 0
@ -1071,7 +1071,7 @@ theorem mul_eq_one {n m : ℕ} (H : n * m = 1) : n = 1 ∧ m = 1
-------------------------------------------------- sub
definition sub (n m : ℕ) : ℕ := nat_rec n (fun m x, pred x) m
definition sub (n m : ℕ) : ℕ := nat.rec n (fun m x, pred x) m
infixl `-`:65 := sub
theorem sub_zero_right (n : ℕ) : n - 0 = n
theorem sub_succ_right (n m : ℕ) : n - succ m = pred (n - m)

6
tests/lean/slow/path_groupoids.lean
View file

@ -24,7 +24,7 @@ notation `idp`:max := idpath _ -- TODO: can we / should we use `1`?
namespace path
abbreviation induction_on {A : Type} {a b : A} (p : a ≈ b)
{C : Π (b : A) (p : a ≈ b), Type} (H : C a (idpath a)) : C b p :=
path_rec H p
path.rec H p
end path
open path
@ -33,11 +33,11 @@ open path
-- -------------------------
definition concat {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : x ≈ z :=
path_rec (λu, u) q p
path.rec (λu, u) q p
-- TODO: should this be an abbreviation?
definition inverse {A : Type} {x y : A} (p : x ≈ y) : y ≈ x :=
path_rec (idpath x) p
path.rec (idpath x) p
infixl `@`:75 := concat
postfix `^`:100 := inverse

2
tests/lua/ac.lua
View file

@ -14,4 +14,4 @@ function display_type(env, t)
print(tostring(t) .. " : " .. tostring(type_checker(env):infer(t)))
end
display_type(env, Const("Acc_rec", {1}))
display_type(env, Const({"Acc", "rec"}, {1}))

6
tests/lua/acc.lua
View file

@ -20,7 +20,7 @@ env = env:add_universe("u")
env = env:add_universe("v")
local u = global_univ("u")
local v = global_univ("v")
display_type(env, Const("Acc_rec", {v, u}))
display_type(env, Const({"Acc", "rec"}, {v, u}))
-- well_founded_induction_type :
-- Pi (A : Type)
@ -34,7 +34,7 @@ local l1 = param_univ("l1")
local l2 = param_univ("l2")
local Acc = Const("Acc", {l1})
local Acc_intro = Const("Acc_intro", {l1})
local Acc_rec = Const("Acc_rec", {l2, l1})
local Acc_rec = Const({"Acc", "rec"}, {l2, l1})
local A = Local("A", mk_sort(l1))
local R = Local("R", mk_arrow(A, A, Prop))
local x = Local("x", A)
@ -61,5 +61,3 @@ local wfi_th_val = Fun(A, R, Hwf, P, H, a, Acc_rec(A, R,
print(env:normalize(type_checker(env):check(wfi_th_val, {l1, l2})))
env = add_decl(env, mk_definition("well_founded_induction_type", {l1, l2}, wfi_th_type, wfi_th_val))
display_type(env, Const("well_founded_induction_type", {1,1}))

8
tests/lua/alias1.lua
View file

@ -30,11 +30,11 @@ env = add_inductive(env,
name("list", "cons"), Pi(A, mk_arrow(A, list_l(A), list_l(A))))
env = add_aliases(env, "list", "lst")
print(not get_expr_aliases(env, {"lst", "list_rec"}):is_nil())
print(not get_expr_aliases(env, {"lst", "list", "rec"}):is_nil())
env = add_aliases(env, "list")
print(get_expr_aliases(env, "list_rec"):head())
assert(not get_expr_aliases(env, "list_rec"):is_nil())
assert(not get_expr_aliases(env, {"lst", "list_rec"}):is_nil())
print(get_expr_aliases(env, {"list", "rec"}):head())
assert(not get_expr_aliases(env, {"list", "rec"}):is_nil())
assert(not get_expr_aliases(env, {"lst", "list", "rec"}):is_nil())
env = add_aliases(env, "list", "l")
print(get_expr_aliases(env, {"l", "list"}):head())

28
tests/lua/ind1.lua
View file

@ -72,9 +72,9 @@ local tc = type_checker(env)
display_type(env, Const("forest", {0}))
display_type(env, Const("vcons", {0}))
display_type(env, Const("consf", {0}))
display_type(env, Const("forest_rec", {v, u}))
display_type(env, Const("nat_rec", {v}))
display_type(env, Const("or_rec"))
display_type(env, Const({"forest", "rec"}, {v, u}))
display_type(env, Const({"nat", "rec"}, {v}))
display_type(env, Const({"or", "rec"}))
local Even = Const("Even")
local Odd = Const("Odd")
@ -100,16 +100,16 @@ local b = Local("b", A)
env = add_inductive(env,
"eq", {l}, 2, Pi(A, a, b, Prop),
"refl", Pi(A, a, eq_l(A, a, a)))
display_type(env, Const("eq_rec", {v, u}))
display_type(env, Const("exists_rec", {u}))
display_type(env, Const("list_rec", {v, u}))
display_type(env, Const("Even_rec"))
display_type(env, Const("Odd_rec"))
display_type(env, Const("and_rec", {v}))
display_type(env, Const("vec_rec", {v, u}))
display_type(env, Const("flist_rec", {v, u}))
display_type(env, Const({"eq", "rec"}, {v, u}))
display_type(env, Const({"exists", "rec"}, {u}))
display_type(env, Const({"list", "rec"}, {v, u}))
display_type(env, Const({"Even", "rec"}))
display_type(env, Const({"Odd", "rec"}))
display_type(env, Const({"and", "rec"}, {v}))
display_type(env, Const({"vec", "rec"}, {v, u}))
display_type(env, Const({"flist", "rec"}, {v, u}))
local nat_rec1 = Const("nat_rec", {1})
local nat_rec1 = Const({"nat", "rec"}, {1})
local a = Local("a", Nat)
local b = Local("b", Nat)
local n = Local("n", Nat)
@ -123,7 +123,7 @@ assert(tc:is_def_eq(add(succ(succ(succ(zero))), succ(succ(zero))),
succ(succ(succ(succ(succ(zero)))))))
local list_nat = Const("list", {1})(Nat)
local list_nat_rec1 = Const("list_rec", {1, 1})(Nat)
local list_nat_rec1 = Const({"list", "rec"}, {1, 1})(Nat)
display_type(env, list_nat_rec1)
local h = Local("h", Nat)
local t = Local("t", list_nat)
@ -155,4 +155,4 @@ env = env:add_universe("v")
env = add_inductive(env,
"Id", {l}, 1, Pi(A, a, b, U_l),
"Id_refl", Pi(A, b, Id_l(A, b, b)))
display_type(env, Const("Id_rec", {v, u}))
display_type(env, Const({"Id", "rec"}, {v, u}))

4
tests/lua/ind3.lua
View file

@ -16,7 +16,7 @@ local a = Local("a", nat)
local b = Local("b", nat)
local n = Local("n", nat)
local r = Local("r", nat)
local nat_rec_nat = Const("nat_rec", {1})(Fun(a, nat))
local nat_rec_nat = Const({"nat", "rec"}, {1})(Fun(a, nat))
local add = Fun(a, b, nat_rec_nat(b, Fun(n, r, succ(r)), a))
local tc = type_checker(env)
assert(tc:is_def_eq(add(succ(succ(zero)), succ(zero)),
@ -48,7 +48,7 @@ local tree_nat = Const("tree", {1})(nat)
local tree_list_nat = Const("tree_list", {1})(nat)
local t = Local("t", tree_nat)
local tl = Local("tl", tree_list_nat)
local tree_rec_nat = Const("tree_rec", {1, 1})(nat, Fun(t, nat), Fun(tl, nat))
local tree_rec_nat = Const({"tree", "rec"}, {1, 1})(nat, Fun(t, nat), Fun(tl, nat))
local r1 = Local("r1", nat)
local r2 = Local("r2", nat)
local length_tree_nat = Fun(t, tree_rec_nat(zero,

8
tests/lua/ind4.lua
View file

@ -14,7 +14,7 @@ local env1 = add_inductive(env,
"nil", Pi(A, list_l(A)),
"cons", Pi(A, mk_arrow(A, list_l(A), list_l(A))))
display_type(env1, Const("list_rec", {1, 1}))
display_type(env1, Const({"list", "rec"}, {1, 1}))
-- Slightly different definition where A : Type.{l} is an index
-- instead of a global parameter
@ -23,8 +23,4 @@ local env2 = add_inductive(env,
"list", {l}, 0, Pi(A, U_sl), -- The resultant type must live in the universe succ(l)
"nil", Pi(A, list_l(A)),
"cons", Pi(A, mk_arrow(A, list_l(A), list_l(A))))
display_type(env2, Const("list_rec", {1, 1}))
display_type(env2, Const({"list", "rec"}, {1, 1}))

2
tests/lua/ind5.lua
View file

@ -15,7 +15,7 @@ env = env:add_universe("u")
local a = Local("a", Prop)
local r = Local("r", retraction)
local rec = Const("retraction_rec")
local rec = Const({"retraction", "rec"})
display_type(env, rec)
local proj = Fun(r, rec(Prop, Fun(a, a), r))
local inj = Const("inj")

2
tests/lua/ind_ex.lua
View file

@ -13,4 +13,4 @@ function display_type(env, t)
print(tostring(t) .. " : " .. tostring(type_checker(env):check(t)))
end
display_type(env, Const("inhabited_rec", {1}))
display_type(env, Const({"inhabited", "rec"}, {1}))

2
tests/lua/ind_tricky.lua
View file

@ -12,6 +12,6 @@ function display_type(env, t)
end
env = env:add_universe("u")
local tricky_rec = Const("tricky_rec", {0})
local tricky_rec = Const({"tricky", "rec"}, {0})
display_type(env, tricky_rec)

4
tests/lua/int1.lua
View file

@ -15,5 +15,5 @@ function display_type(env, t)
print(tostring(t) .. " : " .. tostring(type_checker(env):check(t)))
end
display_type(env, Const("nat_rec", {0}))
display_type(env, Const("int_rec", {0}))
display_type(env, Const({"nat", "rec"}, {0}))
display_type(env, Const({"int", "rec"}, {0}))

3
tests/lua/sorted.lua
View file

@ -27,5 +27,4 @@ env = add_inductive(env,
"is_sorted_cons_nil", Pi(A, lt, a, is_sorted_l(A, lt, cons_l(A, a, nil_l(A)))),
"is_sorted_cons_cons", Pi(A, lt, a1, a2, t, Hlt, Hs, is_sorted_l(A, lt, cons_l(A, a1, cons_l(A, a2, t)))))
print(env:find("is_sorted_rec"):type())
print(env:find({"is_sorted", "rec"}):type())