From 5eaf04518be73f15d02807ad9e00bfe9beebb042 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 22 Jul 2014 09:43:18 -0700 Subject: [PATCH] refactor(*): rename Bool to Prop Signed-off-by: Leonardo de Moura --- library/standard/bit.lean | 2 +- library/standard/bool_decidable.lean | 4 +- library/standard/cast.lean | 6 +- library/standard/classical.lean | 80 ++++++++-------- library/standard/decidable.lean | 24 ++--- library/standard/diaconescu.lean | 10 +- library/standard/equivalence.lean | 10 +- library/standard/hilbert.lean | 8 +- library/standard/if.lean | 8 +- library/standard/logic.lean | 128 +++++++++++++------------- library/standard/sum.lean | 2 +- library/standard/wf.lean | 4 +- src/emacs/lean-mode.el | 2 +- src/frontends/lean/builtin_exprs.cpp | 2 +- src/frontends/lean/notation_cmd.cpp | 2 +- src/frontends/lean/pp.cpp | 4 +- src/kernel/converter.cpp | 4 +- src/kernel/environment.h | 8 +- src/kernel/expr.cpp | 10 +- src/kernel/expr.h | 4 +- src/kernel/formatter.cpp | 2 +- src/kernel/inductive/inductive.cpp | 16 ++-- src/kernel/level.h | 2 +- src/kernel/type_checker.cpp | 2 +- src/library/kernel_bindings.cpp | 4 +- src/library/resolve_macro.cpp | 26 +++--- src/tests/frontends/lean/frontend.cpp | 14 +-- src/tests/frontends/lean/parser.cpp | 8 +- src/tests/frontends/lean/scanner.cpp | 6 +- src/tests/kernel/environment.cpp | 38 ++++---- src/tests/kernel/expr.cpp | 8 +- src/tests/kernel/free_vars.cpp | 6 +- src/tests/kernel/metavar.cpp | 24 ++--- src/tests/library/head_map.cpp | 2 +- src/tests/library/tactic/tactic.cpp | 4 +- tests/lean/let1.lean.expected.out | 46 ++++----- tests/lean/run/alias3.lean | 2 +- tests/lean/run/basic.lean | 4 +- tests/lean/run/calc.lean | 2 +- tests/lean/run/class1.lean | 2 +- tests/lean/run/class2.lean | 2 +- tests/lean/run/class3.lean | 2 +- tests/lean/run/class4.lean | 2 +- tests/lean/run/class7.lean | 4 +- tests/lean/run/class8.lean | 10 +- tests/lean/run/coe2.lean | 4 +- tests/lean/run/coe3.lean | 4 +- tests/lean/run/coe4.lean | 4 +- tests/lean/run/coe5.lean | 4 +- tests/lean/run/e1.lean | 8 +- tests/lean/run/e2.lean | 4 +- tests/lean/run/e3.lean | 10 +- tests/lean/run/e4.lean | 12 +-- tests/lean/run/e5.lean | 20 ++-- tests/lean/run/elim.lean | 2 +- tests/lean/run/elim2.lean | 2 +- tests/lean/run/have1.lean | 4 +- tests/lean/run/have2.lean | 4 +- tests/lean/run/have3.lean | 4 +- tests/lean/run/have4.lean | 4 +- tests/lean/run/have5.lean | 2 +- tests/lean/run/have6.lean | 8 +- tests/lean/run/id.lean | 2 +- tests/lean/run/ind5.lean | 4 +- tests/lean/run/induniv.lean | 6 +- tests/lean/run/is_nil.lean | 10 +- tests/lean/run/n3.lean | 8 +- tests/lean/run/n4.lean | 10 +- tests/lean/run/root.lean | 6 +- tests/lean/run/simple.lean | 10 +- tests/lean/run/t1.lean | 18 ++-- tests/lean/run/tactic1.lean | 2 +- tests/lean/run/tactic10.lean | 2 +- tests/lean/run/tactic11.lean | 2 +- tests/lean/run/tactic12.lean | 2 +- tests/lean/run/tactic13.lean | 2 +- tests/lean/run/tactic14.lean | 2 +- tests/lean/run/tactic2.lean | 2 +- tests/lean/run/tactic21.lean | 4 +- tests/lean/run/tactic22.lean | 2 +- tests/lean/run/tactic23.lean | 2 +- tests/lean/run/tactic24.lean | 4 +- tests/lean/run/tactic25.lean | 4 +- tests/lean/run/tactic3.lean | 2 +- tests/lean/run/tactic4.lean | 4 +- tests/lean/run/tactic5.lean | 2 +- tests/lean/run/tactic6.lean | 2 +- tests/lean/run/tactic7.lean | 4 +- tests/lean/run/tactic8.lean | 2 +- tests/lean/run/tactic9.lean | 2 +- tests/lean/run/uni.lean | 4 +- tests/lean/run/uni2.lean | 4 +- tests/lean/t1.lean | 2 +- tests/lean/t1.lean.expected.out | 2 +- tests/lean/t4.lean | 6 +- tests/lean/t4.lean.expected.out | 8 +- tests/lean/t6.lean | 8 +- tests/lean/t6.lean.expected.out | 4 +- tests/lean/t7.lean | 14 +-- tests/lean/t7.lean.expected.out | 8 +- tests/lua/ac.lua | 4 +- tests/lua/acc.lua | 6 +- tests/lua/alias1.lua | 4 +- tests/lua/alias3.lua | 6 +- tests/lua/choice2.lua | 4 +- tests/lua/cnstr1.lua | 2 +- tests/lua/def1.lua | 4 +- tests/lua/env11.lua | 6 +- tests/lua/env3.lua | 4 +- tests/lua/env4.lua | 2 +- tests/lua/env6.lua | 4 +- tests/lua/env9.lua | 6 +- tests/lua/eta.lua | 8 +- tests/lua/expr10.lua | 8 +- tests/lua/expr2.lua | 18 ++-- tests/lua/expr3.lua | 48 +++++----- tests/lua/expr9.lua | 6 +- tests/lua/goal1.lua | 4 +- tests/lua/ind1.lua | 28 +++--- tests/lua/ind2.lua | 10 +- tests/lua/ind4.lua | 2 +- tests/lua/ind5.lua | 8 +- tests/lua/ind_ex.lua | 2 +- tests/lua/ind_tricky.lua | 4 +- tests/lua/jst1.lua | 2 +- tests/lua/mod1.lua | 12 +-- tests/lua/mod5.lua | 8 +- tests/lua/place2.lua | 4 +- tests/lua/proof_state1.lua | 2 +- tests/lua/res1.lua | 16 ++-- tests/lua/sexpr_bug1.lua | 18 ++-- tests/lua/slow/mod2.lua | 2 +- tests/lua/sorted.lua | 6 +- tests/lua/subst1.lua | 4 +- tests/lua/tactic1.lua | 2 +- tests/lua/tag1.lua | 2 +- tests/lua/tc1.lua | 4 +- tests/lua/tc2.lua | 4 +- tests/lua/tc4.lua | 6 +- tests/lua/tc5.lua | 14 +-- tests/lua/tc_bug1.lua | 14 +-- tests/lua/unify1.lua | 8 +- tests/lua/unify4.lua | 2 +- tests/lua/unify7.lua | 4 +- 144 files changed, 587 insertions(+), 587 deletions(-) diff --git a/library/standard/bit.lean b/library/standard/bit.lean index 2ce617365..bbabe1911 100644 --- a/library/standard/bit.lean +++ b/library/standard/bit.lean @@ -10,7 +10,7 @@ inductive bit : Type := notation `'0`:max := b0 notation `'1`:max := b1 -theorem induction_on {p : bit → Bool} (b : bit) (H0 : p '0) (H1 : p '1) : p b +theorem induction_on {p : bit → Prop} (b : bit) (H0 : p '0) (H1 : p '1) : p b := bit_rec H0 H1 b theorem inhabited_bit [instance] : inhabited bit diff --git a/library/standard/bool_decidable.lean b/library/standard/bool_decidable.lean index 2f4f27318..7ffae64e3 100644 --- a/library/standard/bool_decidable.lean +++ b/library/standard/bool_decidable.lean @@ -7,12 +7,12 @@ using decidable -- Excluded middle + Hilbert implies every proposition is decidable -- First, we show that (decidable a) is inhabited for any 'a' using the excluded middle -theorem inhabited_decidable [instance] (a : Bool) : inhabited (decidable a) +theorem inhabited_decidable [instance] (a : Prop) : inhabited (decidable a) := or_elim (em a) (assume Ha, inhabited_intro (inl Ha)) (assume Hna, inhabited_intro (inr Hna)) -- Note that inhabited_decidable is marked as an instance, and it is silently used -- for synthesizing the implicit argument in the following 'epsilon' -theorem bool_decidable [instance] (a : Bool) : decidable a +theorem bool_decidable [instance] (a : Prop) : decidable a := epsilon (λ d, true) diff --git a/library/standard/cast.lean b/library/standard/cast.lean index 2875c023b..4ed86ecb2 100644 --- a/library/standard/cast.lean +++ b/library/standard/cast.lean @@ -20,7 +20,7 @@ definition heq {A B : Type} (a : A) (b : B) := ∃H, cast H a = b infixl `==`:50 := heq -theorem heq_elim {A B : Type} {C : Bool} {a : A} {b : B} (H1 : a == b) (H2 : ∀ (Hab : A = B), cast Hab a = b → C) : C +theorem heq_elim {A B : Type} {C : Prop} {a : A} {b : B} (H1 : a == b) (H2 : ∀ (Hab : A = B), cast Hab a = b → C) : C := obtain w Hw, from H1, H2 w Hw theorem heq_type_eq {A B : Type} {a : A} {b : B} (H : a == b) : A = B @@ -37,12 +37,12 @@ theorem heq_to_eq {A : Type} {a b : A} (H : a == b) : a = b theorem hrefl {A : Type} (a : A) : a == a := eq_to_heq (refl a) -theorem heqt_elim {a : Bool} (H : a == true) : a +theorem heqt_elim {a : Prop} (H : a == true) : a := eqt_elim (heq_to_eq H) opaque_hint (hiding cast) -theorem hsubst {A B : Type} {a : A} {b : B} {P : ∀ (T : Type), T → Bool} (H1 : a == b) (H2 : P A a) : P B b +theorem hsubst {A B : Type} {a : A} {b : B} {P : ∀ (T : Type), T → Prop} (H1 : a == b) (H2 : P A a) : P B b := have Haux1 : ∀ H : A = A, P A (cast H a), from assume H : A = A, subst (symm (cast_eq H a)) H2, obtain (Heq : A = B) (Hw : cast Heq a = b), from H1, diff --git a/library/standard/classical.lean b/library/standard/classical.lean index f9bbdf9bf..6a10dba6c 100644 --- a/library/standard/classical.lean +++ b/library/standard/classical.lean @@ -3,19 +3,19 @@ -- Author: Leonardo de Moura import logic cast -axiom boolcomplete (a : Bool) : a = true ∨ a = false +axiom propcomplete (a : Prop) : a = true ∨ a = false -theorem case (P : Bool → Bool) (H1 : P true) (H2 : P false) (a : Bool) : P a -:= or_elim (boolcomplete a) +theorem case (P : Prop → Prop) (H1 : P true) (H2 : P false) (a : Prop) : P a +:= or_elim (propcomplete a) (assume Ht : a = true, subst (symm Ht) H1) (assume Hf : a = false, subst (symm Hf) H2) -theorem em (a : Bool) : a ∨ ¬a -:= or_elim (boolcomplete a) +theorem em (a : Prop) : a ∨ ¬a +:= or_elim (propcomplete a) (assume Ht : a = true, or_intro_left (¬ a) (eqt_elim Ht)) (assume Hf : a = false, or_intro_right a (eqf_elim Hf)) -theorem boolcomplete_swapped (a : Bool) : a = false ∨ a = true +theorem propcomplete_swapped (a : Prop) : a = false ∨ a = true := case (λ x, x = false ∨ x = true) (or_intro_right (true = false) (refl true)) (or_intro_left (false = true) (refl false)) @@ -25,15 +25,15 @@ theorem not_true : (¬true) = false := have aux : ¬ (¬true) = true, from not_intro (assume H : (¬true) = true, absurd_not_true (subst (symm H) trivial)), - resolve_right (boolcomplete (¬true)) aux + resolve_right (propcomplete (¬true)) aux theorem not_false : (¬false) = true := have aux : ¬ (¬false) = false, from not_intro (assume H : (¬false) = false, subst H not_false_trivial), - resolve_right (boolcomplete_swapped (¬ false)) aux + resolve_right (propcomplete_swapped (¬ false)) aux -theorem not_not_eq (a : Bool) : (¬¬a) = a +theorem not_not_eq (a : Prop) : (¬¬a) = a := case (λ x, (¬¬x) = x) (calc (¬¬true) = (¬false) : { not_true } ... = true : not_false) @@ -41,39 +41,39 @@ theorem not_not_eq (a : Bool) : (¬¬a) = a ... = false : not_true) a -theorem not_not_elim {a : Bool} (H : ¬¬a) : a +theorem not_not_elim {a : Prop} (H : ¬¬a) : a := (not_not_eq a) ◂ H -theorem boolext {a b : Bool} (Hab : a → b) (Hba : b → a) : a = b -:= or_elim (boolcomplete a) - (assume Hat, or_elim (boolcomplete b) +theorem propext {a b : Prop} (Hab : a → b) (Hba : b → a) : a = b +:= or_elim (propcomplete a) + (assume Hat, or_elim (propcomplete b) (assume Hbt, trans Hat (symm Hbt)) (assume Hbf, false_elim (a = b) (subst Hbf (Hab (eqt_elim Hat))))) - (assume Haf, or_elim (boolcomplete b) + (assume Haf, or_elim (propcomplete b) (assume Hbt, false_elim (a = b) (subst Haf (Hba (eqt_elim Hbt)))) (assume Hbf, trans Haf (symm Hbf))) -theorem iff_to_eq {a b : Bool} (H : a ↔ b) : a = b -:= iff_elim (assume H1 H2, boolext H1 H2) H +theorem iff_to_eq {a b : Prop} (H : a ↔ b) : a = b +:= iff_elim (assume H1 H2, propext H1 H2) H -theorem iff_eq_eq {a b : Bool} : (a ↔ b) = (a = b) -:= boolext +theorem iff_eq_eq {a b : Prop} : (a ↔ b) = (a = b) +:= propext (assume H, iff_to_eq H) (assume H, eq_to_iff H) -theorem eqt_intro {a : Bool} (H : a) : a = true -:= boolext (assume H1 : a, trivial) +theorem eqt_intro {a : Prop} (H : a) : a = true +:= propext (assume H1 : a, trivial) (assume H2 : true, H) -theorem eqf_intro {a : Bool} (H : ¬a) : a = false -:= boolext (assume H1 : a, absurd H1 H) +theorem eqf_intro {a : Prop} (H : ¬a) : a = false +:= propext (assume H1 : a, absurd H1 H) (assume H2 : false, false_elim a H2) -theorem by_contradiction {a : Bool} (H : ¬a → false) : a +theorem by_contradiction {a : Prop} (H : ¬a → false) : a := or_elim (em a) (assume H1 : a, H1) (assume H1 : ¬a, false_elim a (H H1)) theorem a_neq_a {A : Type} (a : A) : (a ≠ a) = false -:= boolext (assume H, a_neq_a_elim H) +:= propext (assume H, a_neq_a_elim H) (assume H, false_elim (a ≠ a) H) theorem eq_id {A : Type} (a : A) : (a = a) = true @@ -82,8 +82,8 @@ theorem eq_id {A : Type} (a : A) : (a = a) = true theorem heq_id {A : Type} (a : A) : (a == a) = true := eqt_intro (hrefl a) -theorem not_or (a b : Bool) : (¬ (a ∨ b)) = (¬ a ∧ ¬ b) -:= boolext +theorem not_or (a b : Prop) : (¬ (a ∨ b)) = (¬ a ∧ ¬ b) +:= propext (assume H, or_elim (em a) (assume Ha, absurd_elim (¬ a ∧ ¬ b) (or_intro_left b Ha) H) (assume Hna, or_elim (em b) @@ -94,8 +94,8 @@ theorem not_or (a b : Bool) : (¬ (a ∨ b)) = (¬ a ∧ ¬ b) (assume Ha, absurd Ha (and_elim_left H)) (assume Hb, absurd Hb (and_elim_right H)))) -theorem not_and (a b : Bool) : (¬ (a ∧ b)) = (¬ a ∨ ¬ b) -:= boolext +theorem not_and (a b : Prop) : (¬ (a ∧ b)) = (¬ a ∨ ¬ b) +:= propext (assume H, or_elim (em a) (assume Ha, or_elim (em b) (assume Hb, absurd_elim (¬ a ∨ ¬ b) (and_intro Ha Hb) H) @@ -106,21 +106,21 @@ theorem not_and (a b : Bool) : (¬ (a ∧ b)) = (¬ a ∨ ¬ b) (assume Hna, absurd (and_elim_left N) Hna) (assume Hnb, absurd (and_elim_right N) Hnb))) -theorem imp_or (a b : Bool) : (a → b) = (¬ a ∨ b) -:= boolext +theorem imp_or (a b : Prop) : (a → b) = (¬ a ∨ b) +:= propext (assume H : a → b, (or_elim (em a) (assume Ha : a, or_intro_right (¬ a) (H Ha)) (assume Hna : ¬ a, or_intro_left b Hna))) (assume (H : ¬ a ∨ b) (Ha : a), resolve_right H ((symm (not_not_eq a)) ◂ Ha)) -theorem not_implies (a b : Bool) : (¬ (a → b)) = (a ∧ ¬b) +theorem not_implies (a b : Prop) : (¬ (a → b)) = (a ∧ ¬b) := calc (¬ (a → b)) = (¬(¬a ∨ b)) : {imp_or a b} ... = (¬¬a ∧ ¬b) : not_or (¬ a) b ... = (a ∧ ¬b) : {not_not_eq a} -theorem a_eq_not_a (a : Bool) : (a = ¬a) = false -:= boolext +theorem a_eq_not_a (a : Prop) : (a = ¬a) = false +:= propext (assume H, or_elim (em a) (assume Ha, absurd Ha (subst H Ha)) (assume Hna, absurd (subst (symm H) Hna) Hna)) @@ -132,24 +132,24 @@ theorem true_eq_false : (true = false) = false theorem false_eq_true : (false = true) = false := subst not_false (a_eq_not_a false) -theorem a_eq_true (a : Bool) : (a = true) = a -:= boolext (assume H, eqt_elim H) (assume H, eqt_intro H) +theorem a_eq_true (a : Prop) : (a = true) = a +:= propext (assume H, eqt_elim H) (assume H, eqt_intro H) -theorem a_eq_false (a : Bool) : (a = false) = ¬a -:= boolext (assume H, eqf_elim H) (assume H, eqf_intro H) +theorem a_eq_false (a : Prop) : (a = false) = ¬a +:= propext (assume H, eqf_elim H) (assume H, eqf_intro H) -theorem not_exists_forall {A : Type} {P : A → Bool} (H : ¬∃x, P x) : ∀x, ¬P x +theorem not_exists_forall {A : Type} {P : A → Prop} (H : ¬∃x, P x) : ∀x, ¬P x := take x, or_elim (em (P x)) (assume Hp : P x, absurd_elim (¬P x) (exists_intro x Hp) H) (assume Hn : ¬P x, Hn) -theorem not_forall_exists {A : Type} {P : A → Bool} (H : ¬∀x, P x) : ∃x, ¬P x +theorem not_forall_exists {A : Type} {P : A → Prop} (H : ¬∀x, P x) : ∃x, ¬P x := by_contradiction (assume H1 : ¬∃ x, ¬P x, have H2 : ∀x, ¬¬P x, from not_exists_forall H1, have H3 : ∀x, P x, from take x, not_not_elim (H2 x), absurd H3 H) -theorem peirce (a b : Bool) : ((a → b) → a) → a +theorem peirce (a b : Prop) : ((a → b) → a) → a := assume H, by_contradiction (assume Hna : ¬a, have Hnna : ¬¬a, from not_implies_left (mt H Hna), absurd (not_not_elim Hnna) Hna) diff --git a/library/standard/decidable.lean b/library/standard/decidable.lean index a4f3a1ad6..5a49b0702 100644 --- a/library/standard/decidable.lean +++ b/library/standard/decidable.lean @@ -4,28 +4,28 @@ import logic namespace decidable -inductive decidable (p : Bool) : Type := +inductive decidable (p : Prop) : Type := | inl : p → decidable p | inr : ¬p → decidable p -theorem induction_on {p : Bool} {C : Bool} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C +theorem induction_on {p : Prop} {C : Prop} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C := decidable_rec H1 H2 H -theorem em (p : Bool) (H : decidable p) : p ∨ ¬p +theorem em (p : Prop) (H : decidable p) : p ∨ ¬p := induction_on H (λ Hp, or_intro_left _ Hp) (λ Hnp, or_intro_right _ Hnp) -definition rec [inline] {p : Bool} {C : Type} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C +definition rec [inline] {p : Prop} {C : Type} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C := decidable_rec H1 H2 H -theorem irrelevant {p : Bool} (d1 d2 : decidable p) : d1 = d2 +theorem irrelevant {p : Prop} (d1 d2 : decidable p) : d1 = d2 := decidable_rec (assume Hp1 : p, decidable_rec - (assume Hp2 : p, congr2 inl (refl Hp1)) -- using proof irrelevance for Bool + (assume Hp2 : p, congr2 inl (refl Hp1)) -- using proof irrelevance for Prop (assume Hnp2 : ¬p, absurd_elim (inl Hp1 = inr Hnp2) Hp1 Hnp2) d2) (assume Hnp1 : ¬p, decidable_rec (assume Hp2 : p, absurd_elim (inr Hnp1 = inl Hp2) Hp2 Hnp1) - (assume Hnp2 : ¬p, congr2 inr (refl Hnp1)) -- using proof irrelevance for Bool + (assume Hnp2 : ¬p, congr2 inr (refl Hnp1)) -- using proof irrelevance for Prop d2) d1 @@ -35,26 +35,26 @@ theorem decidable_true [instance] : decidable true theorem decidable_false [instance] : decidable false := inr not_false_trivial -theorem decidable_and [instance] {a b : Bool} (Ha : decidable a) (Hb : decidable b) : decidable (a ∧ b) +theorem decidable_and [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a ∧ b) := rec Ha (assume Ha : a, rec Hb (assume Hb : b, inl (and_intro Ha Hb)) (assume Hnb : ¬b, inr (and_not_right a Hnb))) (assume Hna : ¬a, inr (and_not_left b Hna)) -theorem decidable_or [instance] {a b : Bool} (Ha : decidable a) (Hb : decidable b) : decidable (a ∨ b) +theorem decidable_or [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a ∨ b) := rec Ha (assume Ha : a, inl (or_intro_left b Ha)) (assume Hna : ¬a, rec Hb (assume Hb : b, inl (or_intro_right a Hb)) (assume Hnb : ¬b, inr (or_not_intro Hna Hnb))) -theorem decidable_not [instance] {a : Bool} (Ha : decidable a) : decidable (¬a) +theorem decidable_not [instance] {a : Prop} (Ha : decidable a) : decidable (¬a) := rec Ha (assume Ha, inr (not_not_intro Ha)) (assume Hna, inl Hna) -theorem decidable_iff [instance] {a b : Bool} (Ha : decidable a) (Hb : decidable b) : decidable (a ↔ b) +theorem decidable_iff [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a ↔ b) := rec Ha (assume Ha, rec Hb (assume Hb : b, inl (iff_intro (assume H, Hb) (assume H, Ha))) @@ -63,7 +63,7 @@ theorem decidable_iff [instance] {a b : Bool} (Ha : decidable a) (Hb : decidable (assume Hb : b, inr (not_intro (assume H : a ↔ b, absurd (iff_mp_right H Hb) Hna))) (assume Hnb : ¬b, inl (iff_intro (assume Ha, absurd_elim b Ha Hna) (assume Hb, absurd_elim a Hb Hnb)))) -theorem decidable_implies [instance] {a b : Bool} (Ha : decidable a) (Hb : decidable b) : decidable (a → b) +theorem decidable_implies [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a → b) := rec Ha (assume Ha : a, rec Hb (assume Hb : b, inl (assume H, Hb)) diff --git a/library/standard/diaconescu.lean b/library/standard/diaconescu.lean index e059f085e..b03d885af 100644 --- a/library/standard/diaconescu.lean +++ b/library/standard/diaconescu.lean @@ -5,11 +5,11 @@ import logic hilbert funext -- Diaconescu’s theorem -- Show that Excluded middle follows from --- Hilbert's choice operator, function extensionality and Boolean extensionality +-- Hilbert's choice operator, function extensionality and Prop extensionality section -hypothesis boolext ⦃a b : Bool⦄ : (a → b) → (b → a) → a = b +hypothesis propext ⦃a b : Prop⦄ : (a → b) → (b → a) → a = b -parameter p : Bool +parameter p : Prop definition u [private] := epsilon (λ x, x = true ∨ p) @@ -33,13 +33,13 @@ lemma uv_implies_p [private] : ¬(u = v) ∨ p lemma p_implies_uv [private] : p → u = v := assume Hp : p, have Hpred : (λ x, x = true ∨ p) = (λ x, x = false ∨ p), from - funext (take x : Bool, + funext (take x : Prop, have Hl : (x = true ∨ p) → (x = false ∨ p), from assume A, or_intro_right (x = false) Hp, have Hr : (x = false ∨ p) → (x = true ∨ p), from assume A, or_intro_right (x = true) Hp, show (x = true ∨ p) = (x = false ∨ p), from - boolext Hl Hr), + propext Hl Hr), show u = v, from subst Hpred (refl (epsilon (λ x, x = true ∨ p))) diff --git a/library/standard/equivalence.lean b/library/standard/equivalence.lean index faf7fd105..6949fd0b5 100644 --- a/library/standard/equivalence.lean +++ b/library/standard/equivalence.lean @@ -6,22 +6,22 @@ import logic namespace equivalence section parameter {A : Type} - parameter p : A → A → Bool + parameter p : A → A → Prop infix `∼`:50 := p definition reflexive := ∀a, a ∼ a definition symmetric := ∀a b, a ∼ b → b ∼ a definition transitive := ∀a b c, a ∼ b → b ∼ c → a ∼ c end -inductive equivalence {A : Type} (p : A → A → Bool) : Bool := +inductive equivalence {A : Type} (p : A → A → Prop) : Prop := | equivalence_intro : reflexive p → symmetric p → transitive p → equivalence p -theorem equivalence_reflexive [instance] {A : Type} {p : A → A → Bool} (H : equivalence p) : reflexive p +theorem equivalence_reflexive [instance] {A : Type} {p : A → A → Prop} (H : equivalence p) : reflexive p := equivalence_rec (λ r s t, r) H -theorem equivalence_symmetric [instance] {A : Type} {p : A → A → Bool} (H : equivalence p) : symmetric p +theorem equivalence_symmetric [instance] {A : Type} {p : A → A → Prop} (H : equivalence p) : symmetric p := equivalence_rec (λ r s t, s) H -theorem equivalence_transitive [instance] {A : Type} {p : A → A → Bool} (H : equivalence p) : transitive p +theorem equivalence_transitive [instance] {A : Type} {p : A → A → Prop} (H : equivalence p) : transitive p := equivalence_rec (λ r s t, t) H end \ No newline at end of file diff --git a/library/standard/hilbert.lean b/library/standard/hilbert.lean index d9aedbc0e..1f71beb91 100644 --- a/library/standard/hilbert.lean +++ b/library/standard/hilbert.lean @@ -3,18 +3,18 @@ -- Author: Leonardo de Moura import logic -variable epsilon {A : Type} {H : inhabited A} (P : A → Bool) : A -axiom epsilon_ax {A : Type} {P : A → Bool} (Hex : ∃ a, P a) : P (@epsilon A (inhabited_exists Hex) P) +variable epsilon {A : Type} {H : inhabited A} (P : A → Prop) : A +axiom epsilon_ax {A : Type} {P : A → Prop} (Hex : ∃ a, P a) : P (@epsilon A (inhabited_exists Hex) P) theorem epsilon_singleton {A : Type} (a : A) : @epsilon A (inhabited_intro a) (λ x, x = a) = a := epsilon_ax (exists_intro a (refl a)) -theorem axiom_of_choice {A : Type} {B : A → Type} {R : Π x, B x → Bool} (H : ∀ x, ∃ y, R x y) : ∃ f, ∀ x, R x (f x) +theorem axiom_of_choice {A : Type} {B : A → Type} {R : Π x, B x → Prop} (H : ∀ x, ∃ y, R x y) : ∃ f, ∀ x, R x (f x) := let f [inline] := λ x, @epsilon _ (inhabited_exists (H x)) (λ y, R x y), H [inline] := take x, epsilon_ax (H x) in exists_intro f H -theorem skolem {A : Type} {B : A → Type} {P : Π x, B x → Bool} : (∀ x, ∃ y, P x y) ↔ ∃ f, (∀ x, P x (f x)) +theorem skolem {A : Type} {B : A → Type} {P : Π x, B x → Prop} : (∀ x, ∃ y, P x y) ↔ ∃ f, (∀ x, P x (f x)) := iff_intro (assume H : (∀ x, ∃ y, P x y), axiom_of_choice H) (assume H : (∃ f, (∀ x, P x (f x))), diff --git a/library/standard/if.lean b/library/standard/if.lean index 34c119c7c..8a15aec17 100644 --- a/library/standard/if.lean +++ b/library/standard/if.lean @@ -4,24 +4,24 @@ import decidable tactic using bit decidable tactic -definition ite (c : Bool) {H : decidable c} {A : Type} (t e : A) : A +definition ite (c : Prop) {H : decidable c} {A : Type} (t e : A) : A := rec H (assume Hc, t) (assume Hnc, e) notation `if` c `then` t `else` e:45 := ite c t e -theorem if_pos {c : Bool} {H : decidable c} (Hc : c) {A : Type} (t e : A) : (if c then t else e) = t +theorem if_pos {c : Prop} {H : decidable c} (Hc : c) {A : Type} (t e : A) : (if c then t else e) = t := decidable_rec (assume Hc : c, refl (@ite c (inl Hc) A t e)) (assume Hnc : ¬c, absurd_elim (@ite c (inr Hnc) A t e = t) Hc Hnc) H -theorem if_neg {c : Bool} {H : decidable c} (Hnc : ¬c) {A : Type} (t e : A) : (if c then t else e) = e +theorem if_neg {c : Prop} {H : decidable c} (Hnc : ¬c) {A : Type} (t e : A) : (if c then t else e) = e := decidable_rec (assume Hc : c, absurd_elim (@ite c (inl Hc) A t e = e) Hc Hnc) (assume Hnc : ¬c, refl (@ite c (inr Hnc) A t e)) H -theorem if_t_t (c : Bool) {H : decidable c} {A : Type} (t : A) : (if c then t else t) = t +theorem if_t_t (c : Prop) {H : decidable c} {A : Type} (t : A) : (if c then t else t) = t := decidable_rec (assume Hc : c, refl (@ite c (inl Hc) A t t)) (assume Hnc : ¬c, refl (@ite c (inr Hnc) A t t)) diff --git a/library/standard/logic.lean b/library/standard/logic.lean index edb2010a4..9678ffbd4 100644 --- a/library/standard/logic.lean +++ b/library/standard/logic.lean @@ -1,42 +1,42 @@ -- Copyright (c) 2014 Microsoft Corporation. All rights reserved. -- Released under Apache 2.0 license as described in the file LICENSE. -- Authors: Leonardo de Moura, Jeremy Avigad -definition Bool [inline] := Type.{0} +definition Prop [inline] := Type.{0} -inductive false : Bool := +inductive false : Prop := -- No constructors -theorem false_elim (c : Bool) (H : false) : c +theorem false_elim (c : Prop) (H : false) : c := false_rec c H -inductive true : Bool := +inductive true : Prop := | trivial : true -definition not (a : Bool) := a → false +definition not (a : Prop) := a → false prefix `¬`:40 := not notation `assume` binders `,` r:(scoped f, f) := r notation `take` binders `,` r:(scoped f, f) := r -theorem not_intro {a : Bool} (H : a → false) : ¬a +theorem not_intro {a : Prop} (H : a → false) : ¬a := H -theorem not_elim {a : Bool} (H1 : ¬a) (H2 : a) : false +theorem not_elim {a : Prop} (H1 : ¬a) (H2 : a) : false := H1 H2 -theorem absurd {a : Bool} (H1 : a) (H2 : ¬a) : false +theorem absurd {a : Prop} (H1 : a) (H2 : ¬a) : false := H2 H1 -theorem not_not_intro {a : Bool} (Ha : a) : ¬¬a +theorem not_not_intro {a : Prop} (Ha : a) : ¬¬a := assume Hna : ¬a, absurd Ha Hna -theorem mt {a b : Bool} (H1 : a → b) (H2 : ¬b) : ¬a +theorem mt {a b : Prop} (H1 : a → b) (H2 : ¬b) : ¬a := assume Ha : a, absurd (H1 Ha) H2 -theorem contrapos {a b : Bool} (H : a → b) : ¬ b → ¬ a +theorem contrapos {a b : Prop} (H : a → b) : ¬ b → ¬ a := assume Hnb : ¬b, mt H Hnb -theorem absurd_elim {a : Bool} (b : Bool) (H1 : a) (H2 : ¬a) : b +theorem absurd_elim {a : Prop} (b : Prop) (H1 : a) (H2 : ¬a) : b := false_elim b (absurd H1 H2) theorem absurd_not_true (H : ¬true) : false @@ -45,66 +45,66 @@ theorem absurd_not_true (H : ¬true) : false theorem not_false_trivial : ¬false := assume H : false, H -theorem not_implies_left {a b : Bool} (H : ¬(a → b)) : ¬¬a +theorem not_implies_left {a b : Prop} (H : ¬(a → b)) : ¬¬a := assume Hna : ¬a, absurd (assume Ha : a, absurd_elim b Ha Hna) H -theorem not_implies_right {a b : Bool} (H : ¬(a → b)) : ¬b +theorem not_implies_right {a b : Prop} (H : ¬(a → b)) : ¬b := assume Hb : b, absurd (assume Ha : a, Hb) H -inductive and (a b : Bool) : Bool := +inductive and (a b : Prop) : Prop := | and_intro : a → b → and a b infixr `/\`:35 := and infixr `∧`:35 := and -theorem and_elim {a b c : Bool} (H1 : a → b → c) (H2 : a ∧ b) : c +theorem and_elim {a b c : Prop} (H1 : a → b → c) (H2 : a ∧ b) : c := and_rec H1 H2 -theorem and_elim_left {a b : Bool} (H : a ∧ b) : a +theorem and_elim_left {a b : Prop} (H : a ∧ b) : a := and_rec (λa b, a) H -theorem and_elim_right {a b : Bool} (H : a ∧ b) : b +theorem and_elim_right {a b : Prop} (H : a ∧ b) : b := and_rec (λa b, b) H -theorem and_swap {a b : Bool} (H : a ∧ b) : b ∧ a +theorem and_swap {a b : Prop} (H : a ∧ b) : b ∧ a := and_intro (and_elim_right H) (and_elim_left H) -theorem and_not_left {a : Bool} (b : Bool) (Hna : ¬a) : ¬(a ∧ b) +theorem and_not_left {a : Prop} (b : Prop) (Hna : ¬a) : ¬(a ∧ b) := assume H : a ∧ b, absurd (and_elim_left H) Hna -theorem and_not_right (a : Bool) {b : Bool} (Hnb : ¬b) : ¬(a ∧ b) +theorem and_not_right (a : Prop) {b : Prop} (Hnb : ¬b) : ¬(a ∧ b) := assume H : a ∧ b, absurd (and_elim_right H) Hnb -inductive or (a b : Bool) : Bool := +inductive or (a b : Prop) : Prop := | or_intro_left : a → or a b | or_intro_right : b → or a b infixr `\/`:30 := or infixr `∨`:30 := or -theorem or_elim {a b c : Bool} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c +theorem or_elim {a b c : Prop} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c := or_rec H2 H3 H1 -theorem resolve_right {a b : Bool} (H1 : a ∨ b) (H2 : ¬a) : b +theorem resolve_right {a b : Prop} (H1 : a ∨ b) (H2 : ¬a) : b := or_elim H1 (assume Ha, absurd_elim b Ha H2) (assume Hb, Hb) -theorem resolve_left {a b : Bool} (H1 : a ∨ b) (H2 : ¬b) : a +theorem resolve_left {a b : Prop} (H1 : a ∨ b) (H2 : ¬b) : a := or_elim H1 (assume Ha, Ha) (assume Hb, absurd_elim a Hb H2) -theorem or_swap {a b : Bool} (H : a ∨ b) : b ∨ a +theorem or_swap {a b : Prop} (H : a ∨ b) : b ∨ a := or_elim H (assume Ha, or_intro_right b Ha) (assume Hb, or_intro_left a Hb) -theorem or_not_intro {a b : Bool} (Hna : ¬a) (Hnb : ¬b) : ¬(a ∨ b) +theorem or_not_intro {a b : Prop} (Hna : ¬a) (Hnb : ¬b) : ¬(a ∨ b) := assume H : a ∨ b, or_elim H (assume Ha, absurd_elim _ Ha Hna) (assume Hb, absurd_elim _ Hb Hnb) -inductive eq {A : Type} (a : A) : A → Bool := +inductive eq {A : Type} (a : A) : A → Prop := | refl : eq a a infix `=`:50 := eq -theorem subst {A : Type} {a b : A} {P : A → Bool} (H1 : a = b) (H2 : P a) : P b +theorem subst {A : Type} {a b : A} {P : A → Prop} (H1 : a = b) (H2 : P a) : P b := eq_rec H2 H1 theorem trans {A : Type} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c @@ -133,31 +133,31 @@ theorem congr {A : Type} {B : Type} {f g : A → B} {a b : A} (H1 : f = g) (H2 : theorem equal_f {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) : ∀x, f x = g x := take x, congr1 H x -theorem not_congr {a b : Bool} (H : a = b) : (¬a) = (¬b) +theorem not_congr {a b : Prop} (H : a = b) : (¬a) = (¬b) := congr2 not H -theorem eqmp {a b : Bool} (H1 : a = b) (H2 : a) : b +theorem eqmp {a b : Prop} (H1 : a = b) (H2 : a) : b := subst H1 H2 infixl `<|`:100 := eqmp infixl `◂`:100 := eqmp -theorem eqmpr {a b : Bool} (H1 : a = b) (H2 : b) : a +theorem eqmpr {a b : Prop} (H1 : a = b) (H2 : b) : a := (symm H1) ◂ H2 -theorem eqt_elim {a : Bool} (H : a = true) : a +theorem eqt_elim {a : Prop} (H : a = true) : a := (symm H) ◂ trivial -theorem eqf_elim {a : Bool} (H : a = false) : ¬a +theorem eqf_elim {a : Prop} (H : a = false) : ¬a := not_intro (assume Ha : a, H ◂ Ha) -theorem imp_trans {a b c : Bool} (H1 : a → b) (H2 : b → c) : a → c +theorem imp_trans {a b c : Prop} (H1 : a → b) (H2 : b → c) : a → c := assume Ha, H2 (H1 Ha) -theorem imp_eq_trans {a b c : Bool} (H1 : a → b) (H2 : b = c) : a → c +theorem imp_eq_trans {a b c : Prop} (H1 : a → b) (H2 : b = c) : a → c := assume Ha, H2 ◂ (H1 Ha) -theorem eq_imp_trans {a b c : Bool} (H1 : a = b) (H2 : b → c) : a → c +theorem eq_imp_trans {a b c : Prop} (H1 : a = b) (H2 : b → c) : a → c := assume Ha, H2 (H1 ◂ Ha) definition ne {A : Type} (a b : A) := ¬(a = b) @@ -190,54 +190,54 @@ theorem ne_eq_trans {A : Type} {a b c : A} (H1 : a ≠ b) (H2 : b = c) : a ≠ c calc_trans eq_ne_trans calc_trans ne_eq_trans -definition iff (a b : Bool) := (a → b) ∧ (b → a) +definition iff (a b : Prop) := (a → b) ∧ (b → a) infix `↔`:25 := iff -theorem iff_intro {a b : Bool} (H1 : a → b) (H2 : b → a) : a ↔ b +theorem iff_intro {a b : Prop} (H1 : a → b) (H2 : b → a) : a ↔ b := and_intro H1 H2 -theorem iff_elim {a b c : Bool} (H1 : (a → b) → (b → a) → c) (H2 : a ↔ b) : c +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 : Bool} (H : a ↔ b) : a → b +theorem iff_elim_left {a b : Prop} (H : a ↔ b) : a → b := iff_elim (assume H1 H2, H1) H -theorem iff_elim_right {a b : Bool} (H : a ↔ b) : b → a +theorem iff_elim_right {a b : Prop} (H : a ↔ b) : b → a := iff_elim (assume H1 H2, H2) H -theorem iff_mp_left {a b : Bool} (H1 : a ↔ b) (H2 : a) : b +theorem iff_mp_left {a b : Prop} (H1 : a ↔ b) (H2 : a) : b := (iff_elim_left H1) H2 -theorem iff_mp_right {a b : Bool} (H1 : a ↔ b) (H2 : b) : a +theorem iff_mp_right {a b : Prop} (H1 : a ↔ b) (H2 : b) : a := (iff_elim_right H1) H2 -theorem iff_flip_sign {a b : Bool} (H1 : a ↔ b) : ¬a ↔ ¬b +theorem iff_flip_sign {a b : Prop} (H1 : a ↔ b) : ¬a ↔ ¬b := iff_intro (assume Hna, mt (iff_elim_right H1) Hna) (assume Hnb, mt (iff_elim_left H1) Hnb) -theorem iff_refl (a : Bool) : a ↔ a +theorem iff_refl (a : Prop) : a ↔ a := iff_intro (assume H, H) (assume H, H) -theorem iff_trans {a b c : Bool} (H1 : a ↔ b) (H2 : b ↔ c) : a ↔ c +theorem iff_trans {a b c : Prop} (H1 : a ↔ b) (H2 : b ↔ c) : a ↔ c := iff_intro (assume Ha, iff_mp_left H2 (iff_mp_left H1 Ha)) (assume Hc, iff_mp_right H1 (iff_mp_right H2 Hc)) -theorem iff_symm {a b : Bool} (H : a ↔ b) : b ↔ a +theorem iff_symm {a b : Prop} (H : a ↔ b) : b ↔ a := iff_intro (assume Hb, iff_mp_right H Hb) (assume Ha, iff_mp_left H Ha) calc_trans iff_trans -theorem eq_to_iff {a b : Bool} (H : a = b) : a ↔ b +theorem eq_to_iff {a b : Prop} (H : a = b) : a ↔ b := iff_intro (λ Ha, subst H Ha) (λ Hb, subst (symm H) Hb) -theorem and_comm (a b : Bool) : a ∧ b ↔ b ∧ a +theorem and_comm (a b : Prop) : a ∧ b ↔ b ∧ a := iff_intro (λH, and_swap H) (λH, and_swap H) -theorem and_assoc (a b c : Bool) : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) +theorem and_assoc (a b c : Prop) : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) := iff_intro (assume H, and_intro (and_elim_left (and_elim_left H)) @@ -246,10 +246,10 @@ theorem and_assoc (a b c : Bool) : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) (and_intro (and_elim_left H) (and_elim_left (and_elim_right H))) (and_elim_right (and_elim_right H))) -theorem or_comm (a b : Bool) : a ∨ b ↔ b ∨ a +theorem or_comm (a b : Prop) : a ∨ b ↔ b ∨ a := iff_intro (λH, or_swap H) (λH, or_swap H) -theorem or_assoc (a b c : Bool) : (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) +theorem or_assoc (a b c : Prop) : (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) := iff_intro (assume H, or_elim H (assume H1, or_elim H1 @@ -262,46 +262,46 @@ theorem or_assoc (a b c : Bool) : (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) (assume Hb, or_intro_left c (or_intro_right a Hb)) (assume Hc, or_intro_right _ Hc))) -inductive Exists {A : Type} (P : A → Bool) : Bool := +inductive Exists {A : Type} (P : A → Prop) : Prop := | exists_intro : ∀ (a : A), P a → Exists P notation `∃` binders `,` r:(scoped P, Exists P) := r -theorem exists_elim {A : Type} {p : A → Bool} {B : Bool} (H1 : ∃x, p x) (H2 : ∀ (a : A) (H : p a), B) : B +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 -theorem exists_not_forall {A : Type} {p : A → Bool} (H : ∃x, p x) : ¬∀x, ¬p x +theorem exists_not_forall {A : Type} {p : A → Prop} (H : ∃x, p x) : ¬∀x, ¬p x := assume H1 : ∀x, ¬p x, obtain (w : A) (Hw : p w), from H, absurd Hw (H1 w) -theorem forall_not_exists {A : Type} {p : A → Bool} (H2 : ∀x, p x) : ¬∃x, ¬p x +theorem forall_not_exists {A : Type} {p : A → Prop} (H2 : ∀x, p x) : ¬∃x, ¬p x := assume H1 : ∃x, ¬p x, obtain (w : A) (Hw : ¬p w), from H1, absurd (H2 w) Hw -definition exists_unique {A : Type} (p : A → Bool) := ∃x, p x ∧ ∀y, y ≠ x → ¬ p y +definition exists_unique {A : Type} (p : A → Prop) := ∃x, p x ∧ ∀y, y ≠ x → ¬ p y notation `∃!` binders `,` r:(scoped P, exists_unique P) := r -theorem exists_unique_intro {A : Type} {p : A → Bool} (w : A) (H1 : p w) (H2 : ∀y, y ≠ w → ¬ p y) : ∃!x, p x +theorem exists_unique_intro {A : Type} {p : A → Prop} (w : A) (H1 : p w) (H2 : ∀y, y ≠ w → ¬ p y) : ∃!x, p x := exists_intro w (and_intro H1 H2) -theorem exists_unique_elim {A : Type} {p : A → Bool} {b : Bool} (H2 : ∃!x, p x) (H1 : ∀x, p x → (∀y, y ≠ x → ¬ p y) → b) : b +theorem exists_unique_elim {A : Type} {p : A → Prop} {b : Prop} (H2 : ∃!x, p x) (H1 : ∀x, p x → (∀y, y ≠ x → ¬ p y) → b) : b := obtain w Hw, from H2, H1 w (and_elim_left Hw) (and_elim_right Hw) -inductive inhabited (A : Type) : Bool := +inductive inhabited (A : Type) : Prop := | inhabited_intro : A → inhabited A -theorem inhabited_elim {A : Type} {B : Bool} (H1 : inhabited A) (H2 : A → B) : B +theorem inhabited_elim {A : Type} {B : Prop} (H1 : inhabited A) (H2 : A → B) : B := inhabited_rec H2 H1 -theorem inhabited_Bool [instance] : inhabited Bool +theorem inhabited_Prop [instance] : inhabited Prop := inhabited_intro true theorem inhabited_fun [instance] (A : Type) {B : Type} (H : inhabited B) : inhabited (A → B) := inhabited_elim H (take b, inhabited_intro (λa, b)) -theorem inhabited_exists {A : Type} {p : A → Bool} (H : ∃x, p x) : inhabited A +theorem inhabited_exists {A : Type} {p : A → Prop} (H : ∃x, p x) : inhabited A := obtain w Hw, from H, inhabited_intro w diff --git a/library/standard/sum.lean b/library/standard/sum.lean index a1573341d..b61e2f4ac 100644 --- a/library/standard/sum.lean +++ b/library/standard/sum.lean @@ -10,6 +10,6 @@ inductive sum (A : Type) (B : Type) : Type := infixr `+`:25 := sum -theorem induction_on {A : Type} {B : Type} {C : Bool} (s : A + B) (H1 : A → C) (H2 : B → C) : C +theorem induction_on {A : Type} {B : Type} {C : Prop} (s : A + B) (H1 : A → C) (H2 : B → C) : C := sum_rec H1 H2 s end \ No newline at end of file diff --git a/library/standard/wf.lean b/library/standard/wf.lean index fd5a7ccb1..df0e4bc55 100644 --- a/library/standard/wf.lean +++ b/library/standard/wf.lean @@ -6,11 +6,11 @@ import logic classical -- Well-founded relation definition -- We are essentially saying that a relation R is well-founded -- if every non-empty "set" P, has a R-minimal element -definition wf {A : Type} (R : A → A → Bool) : Bool +definition wf {A : Type} (R : A → A → Prop) : Prop := ∀P, (∃w, P w) → ∃min, P min ∧ ∀b, R b min → ¬P b -- Well-founded induction theorem -theorem wf_induction {A : Type} {R : A → A → Bool} {P : A → Bool} (Hwf : wf R) (iH : ∀x, (∀y, R y x → P y) → P x) +theorem wf_induction {A : Type} {R : A → A → Prop} {P : A → Prop} (Hwf : wf R) (iH : ∀x, (∀y, R y x → P y) → P x) : ∀x, P x := by_contradiction (assume N : ¬∀x, P x, obtain (w : A) (Hw : ¬P w), from not_forall_exists N, diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el index fe9541fe0..22a2d2109 100644 --- a/src/emacs/lean-mode.el +++ b/src/emacs/lean-mode.el @@ -25,7 +25,7 @@ 'lean-mode ;; name of the mode to create '("--") ;; comments start with '("import" "abbreviation" "opaque_hint" "tactic_hint" "definition" "hiding" "exposing" "parameter" "parameters" "proof" "qed" "conjecture" "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem" "axiom" "inductive" "with" "universe" "alias" "help" "environment" "options" "precedence" "postfix" "prefix" "calc_trans" "calc_subst" "calc_refl" "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" "using" "namespace" "builtin" "including" "class" "instance" "section" "set_option" "add_rewrite") ;; some keywords - '(("\\_<\\(Bool\\|Int\\|Nat\\|Real\\|Type\\|TypeU\\|ℕ\\|ℤ\\)\\_>" . 'font-lock-type-face) + '(("\\_<\\(bool\\|int\\|nat\\|real\\|Prop\\|Type\\|ℕ\\|ℤ\\)\\_>" . 'font-lock-type-face) ("\\_<\\(calc\\|have\\|obtains\\|show\\|by\\|in\\|let\\|forall\\|fun\\|exists\\|if\\|then\\|else\\|assume\\|take\\|obtain\\|from\\)\\_>" . font-lock-keyword-face) ("\"[^\"]*\"" . 'font-lock-string-face) ("\\(->\\|↔\\|/\\\\\\|==\\|\\\\/\\|[*+/<=>¬∧∨≠≤≥-]\\)" . 'font-lock-constant-face) diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 5266ebb8d..303fd1204 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -283,7 +283,7 @@ static name g_exists_elim("exists_elim"); static expr parse_obtain(parser & p, unsigned, expr const *, pos_info const & pos) { if (!p.env().find(g_exists_elim)) throw parser_error("invalid use of 'obtain' expression, environment does not contain 'exists_elim' theorem", pos); - // exists_elim {A : Type} {P : A → Bool} {B : Bool} (H1 : ∃ x : A, P x) (H2 : ∀ (a : A) (H : P a), B) + // exists_elim {A : Type} {P : A → Prop} {B : Prop} (H1 : ∃ x : A, P x) (H2 : ∀ (a : A) (H : P a), B) buffer ps; auto b_pos = p.pos(); environment env = p.parse_binders(ps); diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp index ead5333ba..d2ad4257e 100644 --- a/src/frontends/lean/notation_cmd.cpp +++ b/src/frontends/lean/notation_cmd.cpp @@ -177,7 +177,7 @@ static expr parse_notation_expr(parser & p, buffer const & locals) { return abstract(r, locals.size(), locals.data()); } -static expr g_local_type = mk_Bool(); // type used in notation local declarations, it is irrelevant +static expr g_local_type = mk_Prop(); // type used in notation local declarations, it is irrelevant static void parse_notation_local(parser & p, buffer & locals) { if (p.curr_is_identifier()) { diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 44d978c0d..56b405bb1 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -146,8 +146,8 @@ auto pretty_fn::pp_var(expr const & e) -> result { } auto pretty_fn::pp_sort(expr const & e) -> result { - if (m_env.impredicative() && e == Bool) { - return mk_result(format("Bool")); + if (m_env.impredicative() && e == Prop) { + return mk_result(format("Prop")); } else if (m_universes) { return mk_result(group(format({format("Type.{"), nest(6, pp_level(sort_level(e))), format("}")}))); } else { diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp index 5f23f4e92..104a2a1bd 100644 --- a/src/kernel/converter.cpp +++ b/src/kernel/converter.cpp @@ -496,7 +496,7 @@ struct default_converter : public converter { } if (m_env.prop_proof_irrel()) { - // Proof irrelevance support for Prop/Bool (aka Type.{0}) + // Proof irrelevance support for Prop (aka Type.{0}) type_checker::scope scope(c); expr t_type = infer_type(c, t); if (is_prop(t_type, c) && is_def_eq(t_type, infer_type(c, s), c, jst)) { @@ -532,7 +532,7 @@ struct default_converter : public converter { } bool is_prop(expr const & e, type_checker & c) { - return whnf(infer_type(c, e), c) == Bool; + return whnf(infer_type(c, e), c) == Prop; } }; diff --git a/src/kernel/environment.h b/src/kernel/environment.h index fc9de6987..e0224ca03 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -52,9 +52,9 @@ class environment_header { allow us to add declarations without type checking them (e.g., m_trust_lvl > LEAN_BELIEVER_TRUST_LEVEL) */ unsigned m_trust_lvl; - bool m_prop_proof_irrel; //!< true if the kernel assumes proof irrelevance for Bool/Type (aka Type.{0}) + bool m_prop_proof_irrel; //!< true if the kernel assumes proof irrelevance for Prop (aka Type.{0}) bool m_eta; //!< true if the kernel uses eta-reduction in convertability checks - bool m_impredicative; //!< true if the kernel should treat (universe level 0) as a impredicative Prop/Bool. + bool m_impredicative; //!< true if the kernel should treat (universe level 0) as a impredicative Prop. list m_cls_proof_irrel; //!< list of proof irrelevant classes, if we want Id types to be proof irrelevant, we the name 'Id' in this list. std::unique_ptr m_norm_ext; void dealloc(); @@ -140,7 +140,7 @@ public: /** \brief Return the trust level of this environment. */ unsigned trust_lvl() const { return m_header->trust_lvl(); } - /** \brief Return true iff the environment assumes proof irrelevance for Type.{0} (i.e., Bool) */ + /** \brief Return true iff the environment assumes proof irrelevance for Type.{0} (i.e., Prop) */ bool prop_proof_irrel() const { return m_header->prop_proof_irrel(); } /** \brief Return the list of classes marked as proof irrelevant */ @@ -149,7 +149,7 @@ public: /** \brief Return true iff the environment assumes Eta-reduction */ bool eta() const { return m_header->eta(); } - /** \brief Return true iff the environment treats universe level 0 as an impredicative Prop/Bool */ + /** \brief Return true iff the environment treats universe level 0 as an impredicative Prop */ bool impredicative() const { return m_header->impredicative(); } /** \brief Return reference to the normalizer extension associatied with this environment. */ diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index c65cf458f..335db1184 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -457,10 +457,10 @@ expr mk_pi(unsigned sz, expr const * domain, expr const & range) { return r; } -expr mk_Bool() { - static optional Bool; - if (!Bool) Bool = mk_sort(mk_level_zero()); - return *Bool; +expr mk_Prop() { + static optional Prop; + if (!Prop) Prop = mk_sort(mk_level_zero()); + return *Prop; } expr mk_Type() { @@ -469,7 +469,7 @@ expr mk_Type() { return *Type; } -expr Bool = mk_Bool(); +expr Prop = mk_Prop(); expr Type = mk_Type(); unsigned get_depth(expr const & e) { diff --git a/src/kernel/expr.h b/src/kernel/expr.h index a0c32244e..f5d96239e 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -460,10 +460,10 @@ expr mk_sort(level const & l); expr mk_pi(unsigned sz, expr const * domain, expr const & range); inline expr mk_pi(buffer const & domain, expr const & range) { return mk_pi(domain.size(), domain.data(), range); } -expr mk_Bool(); +expr mk_Prop(); expr mk_Type(); extern expr Type; -extern expr Bool; +extern expr Prop; bool is_default_var_name(name const & n); expr mk_arrow(expr const & t, expr const & e); diff --git a/src/kernel/formatter.cpp b/src/kernel/formatter.cpp index dce6a7f13..5fa813bae 100644 --- a/src/kernel/formatter.cpp +++ b/src/kernel/formatter.cpp @@ -112,7 +112,7 @@ struct print_expr_fn { void print_sort(expr const & a) { if (is_zero(sort_level(a))) { if (m_type0_as_bool) - out() << "Bool"; + out() << "Prop"; else out() << "Type"; } else if (m_type0_as_bool && is_one(sort_level(a))) { diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp index 2c5dea150..07ebb8d1c 100644 --- a/src/kernel/inductive/inductive.cpp +++ b/src/kernel/inductive/inductive.cpp @@ -18,10 +18,10 @@ Author: Leonardo de Moura /* The implementation is based on the paper: "Inductive Families", Peter Dybjer, 1997 The main differences are: - - Support for Bool/Prop (when environment is marked as impredicative) + - Support for Prop (when environment is marked as impredicative) - Universe levels - The support for Bool/Prop is based on the paper: "Inductive Definitions in the System Coq: Rules and Properties", + The support for Prop is based on the paper: "Inductive Definitions in the System Coq: Rules and Properties", Christine Paulin-Mohring. Given a sequence of universe levels parameters (m_level_names), each datatype decls have the form @@ -44,7 +44,7 @@ Author: Leonardo de Moura The universe levels of arguments b and u must be smaller than or equal to l_k in I_k. - When the environment is marked as impredicative, then l_k must be 0 (Bool/Prop) or must be different from zero for + When the environment is marked as impredicative, then l_k must be 0 (Prop) or must be different from zero for any instantiation of the universe level parameters (and global level parameters). This module produces an eliminator/recursor for each inductive datatype I_k, it has the form. @@ -232,7 +232,7 @@ struct add_inductive_fn { */ void check_inductive_types() { bool first = true; - bool to_prop = false; // set to true if the inductive datatypes live in Bool/Prop (Type 0) + bool to_prop = false; // set to true if the inductive datatypes live in Prop (Type 0) for (auto d : m_decls) { expr t = inductive_decl_type(d); tc().check(t, m_level_names); @@ -259,7 +259,7 @@ struct add_inductive_fn { throw kernel_exception(m_env, "number of parameters mismatch in inductive datatype declaration"); t = tc().ensure_sort(t); if (m_env.impredicative()) { - // if the environment is impredicative, then the resultant universe is 0 (Bool/Prop), + // if the environment is impredicative, then the resultant universe is 0 (Prop), // or is never zero (under any parameter assignment). if (!is_zero(sort_level(t)) && !is_not_zero(sort_level(t))) throw kernel_exception(m_env, @@ -270,8 +270,8 @@ struct add_inductive_fn { } else { if (is_zero(sort_level(t)) != to_prop) throw kernel_exception(m_env, - "for impredicative environments, if one datatype is in Bool/Prop, " - "then all of them must be in Bool/Prop"); + "for impredicative environments, if one datatype is in Prop, " + "then all of them must be in Prop"); } } m_it_levels.push_back(sort_level(t)); @@ -469,7 +469,7 @@ struct add_inductive_fn { /** \brief Initialize m_elim_level. */ void mk_elim_level() { if (elim_only_at_universe_zero()) { - // environment is impredicative, datatype maps to Bool/Prop, we have more than one introduction rule. + // environment is impredicative, datatype maps to Prop, we have more than one introduction rule. m_elim_level = mk_level_zero(); } else { name l("l"); diff --git a/src/kernel/level.h b/src/kernel/level.h index e81d86f20..bd3013824 100644 --- a/src/kernel/level.h +++ b/src/kernel/level.h @@ -20,7 +20,7 @@ struct level_cell; /** \brief Universe level kinds. - - Zero : Bool/Prop level. In Lean, Bool == (Type zero) + - Zero : It is also Prop level if env.impredicative() is true - Succ(l) : successor level - Max(l1, l2) : maximum of two levels - IMax(l1, l2) : IMax(x, zero) = zero for all x diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 6529b6d42..4011d2ee0 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -399,7 +399,7 @@ bool type_checker::is_def_eq(expr const & t, expr const & s, justification const /** \brief Return true iff \c e is a proposition */ bool type_checker::is_prop(expr const & e) { scope mk_scope(*this); - bool r = whnf(infer_type(e)) == Bool; + bool r = whnf(infer_type(e)) == Prop; if (r) mk_scope.keep(); return r; } diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index cc7977b78..337cee4c0 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -685,8 +685,8 @@ static void open_expr(lua_State * L) { SET_GLOBAL_FUN(enable_expr_caching, "enable_expr_caching"); - push_expr(L, Bool); - lua_setglobal(L, "Bool"); + push_expr(L, Prop); + lua_setglobal(L, "Prop"); push_expr(L, Type); lua_setglobal(L, "Type"); diff --git a/src/library/resolve_macro.cpp b/src/library/resolve_macro.cpp index e64db8c05..d71d9bb55 100644 --- a/src/library/resolve_macro.cpp +++ b/src/library/resolve_macro.cpp @@ -30,7 +30,7 @@ static expr g_var_0(mk_var(0)); /** \brief Resolve macro encodes a simple propositional resolution step. It takes three arguments: - - t : Bool + - t : Prop - H1 : ( ... ∨ t ∨ ...) - H2 : ( ... ∨ (¬ t) ∨ ...) @@ -39,17 +39,17 @@ static expr g_var_0(mk_var(0)); (resolve l ((A ∨ l) ∨ B) ((C ∨ A) ∨ (¬ l))) : (A ∨ (B ∨ C)) The macro assumes the environment contains the declarations - or (a b : Bool) : Bool - not (a : Bool) : Bool - false : Bool + or (a b : Prop) : Prop + not (a : Prop) : Prop + false : Prop It also assumes that the symbol 'or' is opaque. 'not' and 'false' do not need to be opaque. The macro can be expanded into a term built using - or_elim {a b c : Bool} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c - or_intro_left {a : Bool} (H : a) (b : Bool) : a ∨ b - or_intro_right {b : Bool} (a : Bool) (H : b) : a ∨ b - absurd_elim {a : Bool} (b : Bool) (H1 : a) (H2 : ¬ a) : b + or_elim {a b c : Prop} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c + or_intro_left {a : Prop} (H : a) (b : Prop) : a ∨ b + or_intro_right {b : Prop} (a : Prop) (H : b) : a ∨ b + absurd_elim {a : Prop} (b : Prop) (H1 : a) (H2 : ¬ a) : b Thus, the environment must also contain these declarations. Note that there is no classical reasoning being used. Thus, the macro can be used even @@ -167,8 +167,8 @@ public: if (is_or_app(R)) { expr lhs = app_arg(app_fn(R)); expr rhs = app_arg(R); - // or_intro_left {a : Bool} (H : a) (b : Bool) : a ∨ b - // or_intro_right {b : Bool} (a : Bool) (H : b) : a ∨ b + // or_intro_left {a : Prop} (H : a) (b : Prop) : a ∨ b + // or_intro_right {b : Prop} (a : Prop) (H : b) : a ∨ b if (is_def_eq(l, lhs, ctx)) { return g_or_intro_left(l, H, rhs); } else if (is_def_eq(l, rhs, ctx)) { @@ -224,7 +224,7 @@ public: expr C2_1 = lift(C2); expr H2_1 = lift(H2); expr R_1 = lift(R); - // or_elim {a b c : Bool} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c + // or_elim {a b c : Prop} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c return g_or_elim(lhs1, rhs1, R, H1, mk_lambda("H2", lhs1, mk_or_elim_tree1(l_1, not_l_1, lhs1_1, g_var_0, C2_1, H2_1, R_1, ctx)), mk_lambda("H3", rhs1, mk_or_elim_tree1(l_1, not_l_1, rhs1_1, g_var_0, C2_1, H2_1, R_1, ctx))); @@ -247,7 +247,7 @@ public: if (is_or(C2, lhs, rhs)) { return mk_or_elim_tree2(l, H, not_l, lhs, rhs, H2, R, ctx); } else if (is_def_eq(C2, not_l, ctx)) { - // absurd_elim {a : Bool} (b : Bool) (H1 : a) (H2 : ¬ a) : b + // absurd_elim {a : Prop} (b : Prop) (H1 : a) (H2 : ¬ a) : b return g_absurd_elim(l, R, H, H2); } else { return mk_or_intro(C2, H2, R, ctx); @@ -270,7 +270,7 @@ public: expr lhs2_1 = lift(lhs2); expr rhs2_1 = lift(rhs2); expr R_1 = lift(R); - // or_elim {a b c : Bool} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c + // or_elim {a b c : Prop} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c return g_or_elim(lhs2, rhs2, R, H2, mk_lambda("H2", lhs2, mk_or_elim_tree2(l_1, H_1, not_l_1, lhs2_1, g_var_0, R_1, ctx)), mk_lambda("H3", rhs2, mk_or_elim_tree2(l_1, H_1, not_l_1, rhs2_1, g_var_0, R_1, ctx))); diff --git a/src/tests/frontends/lean/frontend.cpp b/src/tests/frontends/lean/frontend.cpp index 17548537b..85ef7f365 100644 --- a/src/tests/frontends/lean/frontend.cpp +++ b/src/tests/frontends/lean/frontend.cpp @@ -65,12 +65,12 @@ static void tst4() { environment env; io_state ios = init_frontend(env); formatter fmt = mk_pp_formatter(env); context c; - c = extend(c, "x", Bool); - c = extend(c, "y", Bool); - c = extend(c, "x", Bool, Var(1)); - c = extend(c, "x", Bool, Var(2)); - c = extend(c, "z", Bool, Var(1)); - c = extend(c, "x", Bool, Var(4)); + c = extend(c, "x", Prop); + c = extend(c, "y", Prop); + c = extend(c, "x", Prop, Var(1)); + c = extend(c, "x", Prop, Var(2)); + c = extend(c, "z", Prop, Var(1)); + c = extend(c, "x", Prop, Var(4)); std::cout << fmt(c) << "\n"; } @@ -136,7 +136,7 @@ static void tst9() { lean_assert(env->get_uvar("l") == level("l")); try { env->get_uvar("l2"); lean_unreachable(); } catch (exception &) {} - env->add_definition("x", Bool, True); + env->add_definition("x", Prop, True); object const & obj = env->get_object("x"); lean_assert(obj.get_name() == "x"); lean_assert(is_bool(obj.get_type())); diff --git a/src/tests/frontends/lean/parser.cpp b/src/tests/frontends/lean/parser.cpp index ddba08810..a35c455ac 100644 --- a/src/tests/frontends/lean/parser.cpp +++ b/src/tests/frontends/lean/parser.cpp @@ -45,7 +45,7 @@ static void parse_error(environment const & env, io_state const & ios, char cons static void tst1() { environment env; io_state ios = init_test_frontend(env); - parse(env, ios, "variable x : Bool variable y : Bool axiom H : x && y || x -> x"); + parse(env, ios, "variable x : Prop variable y : Prop axiom H : x && y || x -> x"); parse(env, ios, "eval true && true"); parse(env, ios, "print true && false eval true && false"); parse(env, ios, "infixl 35 & : and print true & false & false eval true & false"); @@ -66,9 +66,9 @@ static void check(environment const & env, io_state & ios, char const * str, exp static void tst2() { environment env; io_state ios = init_test_frontend(env); - env->add_var("x", Bool); - env->add_var("y", Bool); - env->add_var("z", Bool); + env->add_var("x", Prop); + env->add_var("y", Prop); + env->add_var("z", Prop); expr x = Const("x"); expr y = Const("y"); expr z = Const("z"); check(env, ios, "x && y", And(x, y)); check(env, ios, "x && y || z", Or(And(x, y), z)); diff --git a/src/tests/frontends/lean/scanner.cpp b/src/tests/frontends/lean/scanner.cpp index 2b7310294..df373a4c3 100644 --- a/src/tests/frontends/lean/scanner.cpp +++ b/src/tests/frontends/lean/scanner.cpp @@ -129,7 +129,7 @@ static void tst2() { scan("x.name"); scan("x.foo"); check("x.name", {tk::Identifier}); - check("fun (x : Bool), x", {tk::Keyword, tk::Keyword, tk::Identifier, tk::Keyword, tk::Identifier, + check("fun (x : Prop), x", {tk::Keyword, tk::Keyword, tk::Identifier, tk::Keyword, tk::Identifier, tk::Keyword, tk::Keyword, tk::Identifier}); check_name("x10", name("x10")); // check_name("x.10", name(name("x"), 10)); @@ -160,8 +160,8 @@ static void tst2() { scan("x10 ... (* print('hello') *) have by"); scan("0..1"); check("0..1", {tk::Numeral, tk::Keyword, tk::Keyword, tk::Numeral}); - scan("theorem a : Bool axiom b : Int"); - check("theorem a : Bool axiom b : Int", {tk::CommandKeyword, tk::Identifier, tk::Keyword, tk::Identifier, + scan("theorem a : Prop axiom b : Int"); + check("theorem a : Prop axiom b : Int", {tk::CommandKeyword, tk::Identifier, tk::Keyword, tk::Identifier, tk::CommandKeyword, tk::Identifier, tk::Keyword, tk::Identifier}); scan("foo \"ttk\\\"\" : Int"); check("foo \"ttk\\\"\" : Int", {tk::Identifier, tk::String, tk::Keyword, tk::Identifier}); diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp index 13e0d556f..e2a1ecc96 100644 --- a/src/tests/kernel/environment.cpp +++ b/src/tests/kernel/environment.cpp @@ -25,18 +25,18 @@ formatter mk_formatter(environment const & env) { static void tst1() { environment env1; - auto env2 = add_decl(env1, mk_definition("Bool", level_param_names(), mk_Type(), mk_Bool())); - lean_assert(!env1.find("Bool")); - lean_assert(env2.find("Bool")); - lean_assert(env2.find("Bool")->get_value() == mk_Bool()); + auto env2 = add_decl(env1, mk_definition("Prop", level_param_names(), mk_Type(), mk_Prop())); + lean_assert(!env1.find("Prop")); + lean_assert(env2.find("Prop")); + lean_assert(env2.find("Prop")->get_value() == mk_Prop()); try { - auto env3 = add_decl(env2, mk_definition("Bool", level_param_names(), mk_Type(), mk_Bool())); + auto env3 = add_decl(env2, mk_definition("Prop", level_param_names(), mk_Type(), mk_Prop())); lean_unreachable(); } catch (kernel_exception & ex) { std::cout << "expected error: " << ex.pp(mk_formatter(ex.get_environment())) << "\n"; } try { - auto env4 = add_decl(env2, mk_definition("BuggyBool", level_param_names(), mk_Bool(), mk_Bool())); + auto env4 = add_decl(env2, mk_definition("BuggyProp", level_param_names(), mk_Prop(), mk_Prop())); lean_unreachable(); } catch (kernel_exception & ex) { std::cout << "expected error: " << ex.pp(mk_formatter(ex.get_environment())) << "\n"; @@ -54,7 +54,7 @@ static void tst1() { std::cout << "expected error: " << ex.pp(mk_formatter(ex.get_environment())) << "\n"; } try { - auto env7 = add_decl(env2, mk_definition("foo", level_param_names(), mk_Type() >> mk_Type(), mk_Bool())); + auto env7 = add_decl(env2, mk_definition("foo", level_param_names(), mk_Type() >> mk_Type(), mk_Prop())); lean_unreachable(); } catch (kernel_exception & ex) { std::cout << "expected error: " << ex.pp(mk_formatter(ex.get_environment())) << "\n"; @@ -64,26 +64,26 @@ static void tst1() { auto env3 = add_decl(env2, mk_definition("id", level_param_names(), Pi(A, A >> A), Fun({A, x}, x))); - expr c = mk_local("c", Bool); + expr c = mk_local("c", Prop); expr id = Const("id"); type_checker checker(env3, name_generator("tmp")); - lean_assert(checker.check(id(Bool)) == Bool >> Bool); - lean_assert(checker.whnf(id(Bool, c)) == c); - lean_assert(checker.whnf(id(Bool, id(Bool, id(Bool, c)))) == c); + lean_assert(checker.check(id(Prop)) == Prop >> Prop); + lean_assert(checker.whnf(id(Prop, c)) == c); + lean_assert(checker.whnf(id(Prop, id(Prop, id(Prop, c)))) == c); type_checker checker2(env2, name_generator("tmp")); - lean_assert(checker2.whnf(id(Bool, id(Bool, id(Bool, c)))) == id(Bool, id(Bool, id(Bool, c)))); + lean_assert(checker2.whnf(id(Prop, id(Prop, id(Prop, c)))) == id(Prop, id(Prop, id(Prop, c)))); } static void tst2() { environment env; name base("base"); - env = add_decl(env, mk_var_decl(name(base, 0u), level_param_names(), Bool >> (Bool >> Bool))); - expr x = Local("x", Bool); - expr y = Local("y", Bool); + env = add_decl(env, mk_var_decl(name(base, 0u), level_param_names(), Prop >> (Prop >> Prop))); + expr x = Local("x", Prop); + expr y = Local("y", Prop); for (unsigned i = 1; i <= 100; i++) { expr prev = Const(name(base, i-1)); - env = add_decl(env, mk_definition(env, name(base, i), level_param_names(), Bool >> (Bool >> Bool), + env = add_decl(env, mk_definition(env, name(base, i), level_param_names(), Prop >> (Prop >> Prop), Fun({x, y}, prev(prev(x, y), prev(y, x))))); } expr A = Local("A", Type); @@ -96,13 +96,13 @@ static void tst2() { expr f97 = Const(name(base, 97)); expr f98 = Const(name(base, 98)); expr f3 = Const(name(base, 3)); - expr c1 = mk_local("c1", Bool); - expr c2 = mk_local("c2", Bool); + expr c1 = mk_local("c1", Prop); + expr c2 = mk_local("c2", Prop); expr id = Const("id"); std::cout << checker.whnf(f3(c1, c2)) << "\n"; lean_assert_eq(env.find(name(base, 98))->get_weight(), 98); lean_assert(checker.is_def_eq(f98(c1, c2), f97(f97(c1, c2), f97(c2, c1)))); - lean_assert(checker.is_def_eq(f98(c1, id(Bool, id(Bool, c2))), f97(f97(c1, id(Bool, c2)), f97(c2, c1)))); + lean_assert(checker.is_def_eq(f98(c1, id(Prop, id(Prop, c2))), f97(f97(c1, id(Prop, c2)), f97(c2, c1)))); name_set s; s.insert(name(base, 96)); type_checker checker2(env, name_generator("tmp"), mk_default_converter(env, optional(), true, s)); diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp index ce797aaf1..d4d489b9c 100644 --- a/src/tests/kernel/expr.cpp +++ b/src/tests/kernel/expr.cpp @@ -277,7 +277,7 @@ static void tst15() { expr f = Const("f"); expr x = Var(0); expr a = Local("a", Type); - expr m = mk_metavar("m", Bool); + expr m = mk_metavar("m", Prop); check_serializer(m); lean_assert(has_metavar(m)); lean_assert(has_metavar(f(m))); @@ -308,7 +308,7 @@ static void tst16() { expr f = Const("f"); expr a = Const("a"); check_copy(f(a)); - check_copy(mk_metavar("M", Bool)); + check_copy(mk_metavar("M", Prop)); check_copy(mk_lambda("x", a, Var(0))); check_copy(mk_pi("x", a, Var(0))); } @@ -332,8 +332,8 @@ static void tst17() { static void tst18() { expr f = Const("f"); expr x = Var(0); - expr l = mk_local("m", Bool); - expr m = mk_metavar("m", Bool); + expr l = mk_local("m", Prop); + expr m = mk_metavar("m", Prop); expr a0 = Const("a"); expr a = Local("a", Type); expr a1 = Local("a", m); diff --git a/src/tests/kernel/free_vars.cpp b/src/tests/kernel/free_vars.cpp index 2042b3123..1b4d7e34c 100644 --- a/src/tests/kernel/free_vars.cpp +++ b/src/tests/kernel/free_vars.cpp @@ -32,7 +32,7 @@ static void tst1() { static void tst2() { expr f = Const("f"); - expr B = Const("Bool"); + expr B = Const("Prop"); expr x = Local("x", B); expr y = Local("y", B); expr t = Fun({x, y}, x); @@ -46,7 +46,7 @@ static void tst3() { expr f = Const("f"); expr a = Const("a"); expr r = f(a, Var(m)); - expr b = Const("Bool"); + expr b = Const("Prop"); for (unsigned i = 0; i < n; i++) r = mk_lambda(name(), b, r); lean_assert(closed(r)); @@ -59,7 +59,7 @@ static void tst3() { static void tst4() { expr f = Const("f"); - expr B = Bool; + expr B = Prop; expr x = Local("x", B); expr y = Local("y", B); expr t = f(Fun({x, y}, f(x, y))(f(Var(1), Var(2))), x); diff --git a/src/tests/kernel/metavar.cpp b/src/tests/kernel/metavar.cpp index f5edffcf8..c39c6998e 100644 --- a/src/tests/kernel/metavar.cpp +++ b/src/tests/kernel/metavar.cpp @@ -68,9 +68,9 @@ static bool check_assumptions(justification const & j, std::initializer_list> (Bool >> Bool)); + expr m1 = mk_metavar("m1", Prop >> (Prop >> Prop)); substitution s; expr f = Const("f"); expr g = Const("g"); expr a = Const("a"); expr b = Const("b"); - expr x = Local("x", Bool); - expr y = Local("y", Bool); + expr x = Local("x", Prop); + expr y = Local("y", Prop); s = s.assign(m1, Fun({x, y}, f(y, x))); lean_assert_eq(s.instantiate_metavars(m1(a, b, g(a))).first, f(b, a, g(a))); lean_assert_eq(s.instantiate_metavars(m1(a)).first, Fun(y, f(y, a))); @@ -137,9 +137,9 @@ static void tst3() { } static void tst4() { - expr m1 = mk_metavar("m1", Bool); - expr m2 = mk_metavar("m2", Bool); - expr m3 = mk_metavar("m3", Bool); + expr m1 = mk_metavar("m1", Prop); + expr m2 = mk_metavar("m2", Prop); + expr m3 = mk_metavar("m3", Prop); level l1 = mk_meta_univ("l1"); level u = mk_global_univ("u"); substitution s; @@ -154,7 +154,7 @@ static void tst4() { s = s.assign(m2, m3, justification()); lean_assert(s.instantiate_metavars(t).first == f(T1, T2, a, m3)); s = s.assign(l1, level(), justification()); - lean_assert(s.instantiate_metavars(t).first == f(Bool, T2, a, m3)); + lean_assert(s.instantiate_metavars(t).first == f(Prop, T2, a, m3)); } int main() { diff --git a/src/tests/library/head_map.cpp b/src/tests/library/head_map.cpp index 34b3f2b32..18bbaccc3 100644 --- a/src/tests/library/head_map.cpp +++ b/src/tests/library/head_map.cpp @@ -14,7 +14,7 @@ static void tst1() { expr a = Const("a"); expr f = Const("f"); expr b = Const("b"); - expr x = Local("x", Bool); + expr x = Local("x", Prop); expr l1 = Fun(x, x); expr l2 = Fun(x, f(x)); lean_assert(l1 != l2); diff --git a/src/tests/library/tactic/tactic.cpp b/src/tests/library/tactic/tactic.cpp index e8370d6fd..89d5664ab 100644 --- a/src/tests/library/tactic/tactic.cpp +++ b/src/tests/library/tactic/tactic.cpp @@ -53,8 +53,8 @@ static void tst1() { environment env; io_state io(options(), mk_simple_formatter()); init_test_frontend(env); - env->add_var("p", Bool); - env->add_var("q", Bool); + env->add_var("p", Prop); + env->add_var("q", Prop); expr p = Const("p"); expr q = Const("q"); context ctx; diff --git a/tests/lean/let1.lean.expected.out b/tests/lean/let1.lean.expected.out index 92a3a57a5..eb0dbef4c 100644 --- a/tests/lean/let1.lean.expected.out +++ b/tests/lean/let1.lean.expected.out @@ -1,33 +1,33 @@ -let and_intro : ∀ (p q : Bool), - p → q → (λ (p q : Bool), ∀ (c : Bool), (p → q → c) → c) p q := - λ (p q : Bool) (H1 : p) (H2 : q) (c : Bool) (H : p → q → c), +let and_intro : ∀ (p q : Prop), + p → q → (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q := + λ (p q : Prop) (H1 : p) (H2 : q) (c : Prop) (H : p → q → c), H H1 H2, - and_elim_left : ∀ (p q : Bool), - (λ (p q : Bool), ∀ (c : Bool), (p → q → c) → c) p q → p := - λ (p q : Bool) (H : (λ (p q : Bool), ∀ (c : Bool), (p → q → c) → c) p q), + and_elim_left : ∀ (p q : Prop), + (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q → p := + λ (p q : Prop) (H : (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q), H p (λ (H1 : p) (H2 : q), H1), - and_elim_right : ∀ (p q : Bool), - (λ (p q : Bool), ∀ (c : Bool), (p → q → c) → c) p q → q := - λ (p q : Bool) (H : (λ (p q : Bool), ∀ (c : Bool), (p → q → c) → c) p q), + and_elim_right : ∀ (p q : Prop), + (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q → q := + λ (p q : Prop) (H : (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q), H q (λ (H1 : p) (H2 : q), H2) in and_intro : - ∀ (p q : Bool), - p → q → (λ (p q : Bool), ∀ (c : Bool), (p → q → c) → c) p q + ∀ (p q : Prop), + p → q → (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q let1.lean:17:20: error: type mismatch at application - (λ (and_intro : ∀ (p q : Bool), p → q → (λ (p q : Bool), ∀ (c : Bool), (p → q → c) → c) q p), - let and_elim_left : ∀ (p q : Bool), - (λ (p q : Bool), ∀ (c : Bool), (p → q → c) → c) p q → p := - λ (p q : Bool) (H : (λ (p q : Bool), ∀ (c : Bool), (p → q → c) → c) p q), + (λ (and_intro : ∀ (p q : Prop), p → q → (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) q p), + let and_elim_left : ∀ (p q : Prop), + (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q → p := + λ (p q : Prop) (H : (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q), H p (λ (H1 : p) (H2 : q), H1), - and_elim_right : ∀ (p q : Bool), - (λ (p q : Bool), ∀ (c : Bool), (p → q → c) → c) p q → q := - λ (p q : Bool) (H : (λ (p q : Bool), ∀ (c : Bool), (p → q → c) → c) p q), + and_elim_right : ∀ (p q : Prop), + (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q → q := + λ (p q : Prop) (H : (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q), H q (λ (H1 : p) (H2 : q), H2) in and_intro) - (λ (p q : Bool) (H1 : p) (H2 : q) (c : Bool) (H : p → q → c), H H1 H2) + (λ (p q : Prop) (H1 : p) (H2 : q) (c : Prop) (H : p → q → c), H H1 H2) expected type: - ∀ (p q : Bool), - p → q → (λ (p q : Bool), ∀ (c : Bool), (p → q → c) → c) q p + ∀ (p q : Prop), + p → q → (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) q p given type: - ∀ (p q : Bool), - p → q → (∀ (c : Bool), (p → q → c) → c) + ∀ (p q : Prop), + p → q → (∀ (c : Prop), (p → q → c) → c) diff --git a/tests/lean/run/alias3.lean b/tests/lean/run/alias3.lean index 399e019e3..21dffe4a8 100644 --- a/tests/lean/run/alias3.lean +++ b/tests/lean/run/alias3.lean @@ -4,7 +4,7 @@ namespace N1 section section variable A : Type - definition foo (a : A) : Bool := true + definition foo (a : A) : Prop := true check foo end check foo diff --git a/tests/lean/run/basic.lean b/tests/lean/run/basic.lean index 53454ed71..337dd7741 100644 --- a/tests/lean/run/basic.lean +++ b/tests/lean/run/basic.lean @@ -30,8 +30,8 @@ end check double check double.{1 2} -definition Bool [inline] := Type.{0} -variable eq : Π {A : Type}, A → A → Bool +definition Prop [inline] := Type.{0} +variable eq : Π {A : Type}, A → A → Prop infix `=`:50 := eq check eq.{1} diff --git a/tests/lean/run/calc.lean b/tests/lean/run/calc.lean index 5e44e8229..f0e336f43 100644 --- a/tests/lean/run/calc.lean +++ b/tests/lean/run/calc.lean @@ -2,7 +2,7 @@ import standard using num namespace foo - variable le : num → num → Bool + variable le : num → num → Prop axiom le_trans {a b c : num} : le a b → le b c → le a c calc_trans le_trans infix `≤`:50 := le diff --git a/tests/lean/run/class1.lean b/tests/lean/run/class1.lean index dd72065b7..aa25e295b 100644 --- a/tests/lean/run/class1.lean +++ b/tests/lean/run/class1.lean @@ -1,7 +1,7 @@ import standard using num pair -definition H : inhabited (Bool × num × (num → num)) := _ +definition H : inhabited (Prop × num × (num → num)) := _ (* print(get_env():find("H"):value()) diff --git a/tests/lean/run/class2.lean b/tests/lean/run/class2.lean index cc06516cb..1f30dddff 100644 --- a/tests/lean/run/class2.lean +++ b/tests/lean/run/class2.lean @@ -1,7 +1,7 @@ import standard using num pair -theorem H {A B : Type} (H1 : inhabited A) : inhabited (Bool × A × (B → num)) +theorem H {A B : Type} (H1 : inhabited A) : inhabited (Prop × A × (B → num)) := _ (* diff --git a/tests/lean/run/class3.lean b/tests/lean/run/class3.lean index 2ffc19b93..9c81dd297 100644 --- a/tests/lean/run/class3.lean +++ b/tests/lean/run/class3.lean @@ -9,7 +9,7 @@ section -- The section mechanism only includes parameters that are explicitly cited. -- So, we use the 'including' expression to make explicit we want to use -- Ha and Hb - theorem tst : inhabited (Bool × A × B) + theorem tst : inhabited (Prop × A × B) := including Ha Hb, _ end diff --git a/tests/lean/run/class4.lean b/tests/lean/run/class4.lean index 275fc721c..d099faeaf 100644 --- a/tests/lean/run/class4.lean +++ b/tests/lean/run/class4.lean @@ -53,7 +53,7 @@ theorem not_zero_add (x y : nat) (H : ¬ is_zero y) : ¬ is_zero (x + y) not_is_zero_succ (x+w), subst (symm H1) H2) -inductive not_zero (x : nat) : Bool := +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 diff --git a/tests/lean/run/class7.lean b/tests/lean/run/class7.lean index 5bfc129cf..1538f0de8 100644 --- a/tests/lean/run/class7.lean +++ b/tests/lean/run/class7.lean @@ -6,7 +6,7 @@ inductive inh (A : Type) : Type := instance inh_intro -theorem inh_bool [instance] : inh Bool +theorem inh_bool [instance] : inh Prop := inh_intro true theorem inh_fun [instance] {A B : Type} (H : inh B) : inh (A → B) @@ -22,4 +22,4 @@ theorem tst {A B : Type} (H : inh B) : inh (A → B → B) theorem T1 {A : Type} (a : A) : inh A -theorem T2 : inh Bool +theorem T2 : inh Prop diff --git a/tests/lean/run/class8.lean b/tests/lean/run/class8.lean index 3e9044130..34956fe3c 100644 --- a/tests/lean/run/class8.lean +++ b/tests/lean/run/class8.lean @@ -1,18 +1,18 @@ import standard using num tactic pair -inductive inh (A : Type) : Bool := +inductive inh (A : Type) : Prop := | inh_intro : A -> inh A instance inh_intro -theorem inh_elim {A : Type} {B : Bool} (H1 : inh A) (H2 : A → B) : B +theorem inh_elim {A : Type} {B : Prop} (H1 : inh A) (H2 : A → B) : B := inh_rec H2 H1 -theorem inh_exists [instance] {A : Type} {P : A → Bool} (H : ∃x, P x) : inh A +theorem inh_exists [instance] {A : Type} {P : A → Prop} (H : ∃x, P x) : inh A := obtain w Hw, from H, inh_intro w -theorem inh_bool [instance] : inh Bool +theorem inh_bool [instance] : inh Prop := inh_intro true theorem inh_fun [instance] {A B : Type} (H : inh B) : inh (A → B) @@ -26,7 +26,7 @@ tactic_hint assump theorem tst {A B : Type} (H : inh B) : inh (A → B → B) -theorem T1 {A B C D : Type} {P : C → Bool} (a : A) (H1 : inh B) (H2 : ∃x, P x) : inh ((A → A) × B × (D → C) × Bool) +theorem T1 {A B C D : Type} {P : C → Prop} (a : A) (H1 : inh B) (H2 : ∃x, P x) : inh ((A → A) × B × (D → C) × Prop) (* print(get_env():find("T1"):value()) diff --git a/tests/lean/run/coe2.lean b/tests/lean/run/coe2.lean index 9a7ddc9eb..b2fbd3fb9 100644 --- a/tests/lean/run/coe2.lean +++ b/tests/lean/run/coe2.lean @@ -2,12 +2,12 @@ import standard namespace setoid inductive setoid : Type := - | mk_setoid: Π (A : Type), (A → A → Bool) → setoid + | mk_setoid: Π (A : Type), (A → A → Prop) → setoid definition carrier (s : setoid) := setoid_rec (λ a eq, a) s - definition eqv {s : setoid} : carrier s → carrier s → Bool + definition eqv {s : setoid} : carrier s → carrier s → Prop := setoid_rec (λ a eqv, eqv) s infix `≈`:50 := eqv diff --git a/tests/lean/run/coe3.lean b/tests/lean/run/coe3.lean index 993c9a338..7b8a7ab55 100644 --- a/tests/lean/run/coe3.lean +++ b/tests/lean/run/coe3.lean @@ -2,12 +2,12 @@ import standard namespace setoid inductive setoid : Type := - | mk_setoid: Π (A : Type), (A → A → Bool) → setoid + | mk_setoid: Π (A : Type), (A → A → Prop) → setoid definition carrier (s : setoid) := setoid_rec (λ a eq, a) s - definition eqv {s : setoid} : carrier s → carrier s → Bool + definition eqv {s : setoid} : carrier s → carrier s → Prop := setoid_rec (λ a eqv, eqv) s infix `≈`:50 := eqv diff --git a/tests/lean/run/coe4.lean b/tests/lean/run/coe4.lean index 93996b3b7..a16fa27c0 100644 --- a/tests/lean/run/coe4.lean +++ b/tests/lean/run/coe4.lean @@ -2,7 +2,7 @@ import standard namespace setoid inductive setoid : Type := - | mk_setoid: Π (A : Type'), (A → A → Bool) → setoid + | mk_setoid: Π (A : Type'), (A → A → Prop) → setoid set_option pp.universes true @@ -12,7 +12,7 @@ namespace setoid definition carrier (s : setoid) := setoid_rec (λ a eq, a) s - definition eqv {s : setoid} : carrier s → carrier s → Bool + definition eqv {s : setoid} : carrier s → carrier s → Prop := setoid_rec (λ a eqv, eqv) s infix `≈`:50 := eqv diff --git a/tests/lean/run/coe5.lean b/tests/lean/run/coe5.lean index 8714ec5ae..0b0d7a868 100644 --- a/tests/lean/run/coe5.lean +++ b/tests/lean/run/coe5.lean @@ -2,7 +2,7 @@ import standard namespace setoid inductive setoid : Type := - | mk_setoid: Π (A : Type'), (A → A → Bool) → setoid + | mk_setoid: Π (A : Type'), (A → A → Prop) → setoid set_option pp.universes true @@ -12,7 +12,7 @@ namespace setoid definition carrier (s : setoid) := setoid_rec (λ a eq, a) s - definition eqv {s : setoid} : carrier s → carrier s → Bool + definition eqv {s : setoid} : carrier s → carrier s → Prop := setoid_rec (λ a eqv, eqv) s infix `≈`:50 := eqv diff --git a/tests/lean/run/e1.lean b/tests/lean/run/e1.lean index 6e8f04459..a3496d42b 100644 --- a/tests/lean/run/e1.lean +++ b/tests/lean/run/e1.lean @@ -1,15 +1,15 @@ -definition Bool [inline] : Type.{1} := Type.{0} -variable eq : forall {A : Type}, A → A → Bool +definition Prop [inline] : Type.{1} := Type.{0} +variable eq : forall {A : Type}, A → A → Prop variable N : Type.{1} variables a b c : N infix `=`:50 := eq check a = b -variable f : Bool → N → N +variable f : Prop → N → N variable g : N → N → N precedence `+`:50 infixl + := f infixl + := g check a + b + c -variable p : Bool +variable p : Prop check p + a + b + c diff --git a/tests/lean/run/e2.lean b/tests/lean/run/e2.lean index 2a2a98f7c..0b606100f 100644 --- a/tests/lean/run/e2.lean +++ b/tests/lean/run/e2.lean @@ -1,2 +1,2 @@ -definition Bool [inline] := Type.{0} -check Bool +definition Prop [inline] := Type.{0} +check Prop diff --git a/tests/lean/run/e3.lean b/tests/lean/run/e3.lean index 97ea4302a..5190f7e28 100644 --- a/tests/lean/run/e3.lean +++ b/tests/lean/run/e3.lean @@ -1,13 +1,13 @@ -definition Bool [inline] := Type.{0} +definition Prop [inline] := Type.{0} -definition false := ∀x : Bool, x +definition false := ∀x : Prop, x check false -theorem false_elim (C : Bool) (H : false) : C +theorem false_elim (C : Prop) (H : false) : C := H C definition eq {A : Type} (a b : A) -:= ∀ {P : A → Bool}, P a → P b +:= ∀ {P : A → Prop}, P a → P b check eq @@ -16,6 +16,6 @@ infix `=`:50 := eq theorem refl {A : Type} (a : A) : a = a := λ P H, H -theorem subst {A : Type} {P : A -> Bool} {a b : A} (H1 : a = b) (H2 : P a) : P b +theorem subst {A : Type} {P : A -> Prop} {a b : A} (H1 : a = b) (H2 : P a) : P b := @H1 P H2 diff --git a/tests/lean/run/e4.lean b/tests/lean/run/e4.lean index 13d6ec8db..5265bad9b 100644 --- a/tests/lean/run/e4.lean +++ b/tests/lean/run/e4.lean @@ -1,13 +1,13 @@ -definition Bool [inline] := Type.{0} +definition Prop [inline] := Type.{0} -definition false : Bool := ∀x : Bool, x +definition false : Prop := ∀x : Prop, x check false -theorem false_elim (C : Bool) (H : false) : C +theorem false_elim (C : Prop) (H : false) : C := H C definition eq {A : Type} (a b : A) -:= ∀ P : A → Bool, P a → P b +:= ∀ P : A → Prop, P a → P b check eq @@ -16,13 +16,13 @@ infix `=`:50 := eq theorem refl {A : Type} (a : A) : a = a := λ P H, H -definition true : Bool +definition true : Prop := false = false theorem trivial : true := refl false -theorem subst {A : Type} {P : A -> Bool} {a b : A} (H1 : a = b) (H2 : P a) : P b +theorem subst {A : Type} {P : A -> Prop} {a b : A} (H1 : a = b) (H2 : P a) : P b := H1 _ H2 theorem symm {A : Type} {a b : A} (H : a = b) : b = a diff --git a/tests/lean/run/e5.lean b/tests/lean/run/e5.lean index 319693d6c..393a87015 100644 --- a/tests/lean/run/e5.lean +++ b/tests/lean/run/e5.lean @@ -1,13 +1,13 @@ -definition Bool [inline] := Type.{0} +definition Prop [inline] := Type.{0} -definition false : Bool := ∀x : Bool, x +definition false : Prop := ∀x : Prop, x check false -theorem false_elim (C : Bool) (H : false) : C +theorem false_elim (C : Prop) (H : false) : C := H C definition eq {A : Type} (a b : A) -:= ∀ P : A → Bool, P a → P b +:= ∀ P : A → Prop, P a → P b check eq @@ -16,13 +16,13 @@ infix `=`:50 := eq theorem refl {A : Type} (a : A) : a = a := λ P H, H -definition true : Bool +definition true : Prop := false = false theorem trivial : true := refl false -theorem subst {A : Type} {P : A -> Bool} {a b : A} (H1 : a = b) (H2 : P a) : P b +theorem subst {A : Type} {P : A -> Prop} {a b : A} (H1 : a = b) (H2 : P a) : P b := H1 _ H2 theorem symm {A : Type} {a b : A} (H : a = b) : b = a @@ -36,10 +36,10 @@ inductive nat : Type := | succ : nat → nat print "using strict implicit arguments" -abbreviation symmetric {A : Type} (R : A → A → Bool) := ∀ ⦃a b⦄, R a b → R b a +abbreviation symmetric {A : Type} (R : A → A → Prop) := ∀ ⦃a b⦄, R a b → R b a check symmetric -variable p : nat → nat → Bool +variable p : nat → nat → Prop check symmetric p axiom H1 : symmetric p axiom H2 : p zero (succ zero) @@ -48,7 +48,7 @@ check H1 H2 print "------------" print "using implicit arguments" -abbreviation symmetric2 {A : Type} (R : A → A → Bool) := ∀ {a b}, R a b → R b a +abbreviation symmetric2 {A : Type} (R : A → A → Prop) := ∀ {a b}, R a b → R b a check symmetric2 check symmetric2 p axiom H3 : symmetric2 p @@ -58,7 +58,7 @@ check H3 H4 print "-----------------" print "using strict implicit arguments (ASCII notation)" -abbreviation symmetric3 {A : Type} (R : A → A → Bool) := ∀ {{a b}}, R a b → R b a +abbreviation symmetric3 {A : Type} (R : A → A → Prop) := ∀ {{a b}}, R a b → R b a check symmetric3 check symmetric3 p diff --git a/tests/lean/run/elim.lean b/tests/lean/run/elim.lean index 51786842e..fc88de62c 100644 --- a/tests/lean/run/elim.lean +++ b/tests/lean/run/elim.lean @@ -1,6 +1,6 @@ import standard using num -variable p : num → num → num → Bool +variable p : num → num → num → Prop axiom H1 : ∃ x y z, p x y z axiom H2 : ∀ {x y z : num}, p x y z → p x x x theorem tst : ∃ x, p x x x diff --git a/tests/lean/run/elim2.lean b/tests/lean/run/elim2.lean index 6ed301e5a..90a1d2b1c 100644 --- a/tests/lean/run/elim2.lean +++ b/tests/lean/run/elim2.lean @@ -1,6 +1,6 @@ import standard using num tactic -variable p : num → num → num → Bool +variable p : num → num → num → Prop axiom H1 : ∃ x y z, p x y z axiom H2 : ∀ {x y z : num}, p x y z → p x x x theorem tst : ∃ x, p x x x diff --git a/tests/lean/run/have1.lean b/tests/lean/run/have1.lean index 549d66e6d..799f50c7d 100644 --- a/tests/lean/run/have1.lean +++ b/tests/lean/run/have1.lean @@ -1,5 +1,5 @@ -abbreviation Bool : Type.{1} := Type.{0} -variables a b c : Bool +abbreviation Prop : Type.{1} := Type.{0} +variables a b c : Prop axiom Ha : a axiom Hb : b axiom Hc : c diff --git a/tests/lean/run/have2.lean b/tests/lean/run/have2.lean index 8afd796d9..71ca1ed2d 100644 --- a/tests/lean/run/have2.lean +++ b/tests/lean/run/have2.lean @@ -1,5 +1,5 @@ -abbreviation Bool : Type.{1} := Type.{0} -variables a b c : Bool +abbreviation Prop : Type.{1} := Type.{0} +variables a b c : Prop axiom Ha : a axiom Hb : b axiom Hc : c diff --git a/tests/lean/run/have3.lean b/tests/lean/run/have3.lean index 1339fbb98..57a81f1f1 100644 --- a/tests/lean/run/have3.lean +++ b/tests/lean/run/have3.lean @@ -1,5 +1,5 @@ -abbreviation Bool : Type.{1} := Type.{0} -variables a b c : Bool +abbreviation Prop : Type.{1} := Type.{0} +variables a b c : Prop axiom Ha : a axiom Hb : b axiom Hc : c diff --git a/tests/lean/run/have4.lean b/tests/lean/run/have4.lean index d6e170efa..0c4516639 100644 --- a/tests/lean/run/have4.lean +++ b/tests/lean/run/have4.lean @@ -1,5 +1,5 @@ -abbreviation Bool : Type.{1} := Type.{0} -variables a b c : Bool +abbreviation Prop : Type.{1} := Type.{0} +variables a b c : Prop axiom Ha : a axiom Hb : b axiom Hc : c diff --git a/tests/lean/run/have5.lean b/tests/lean/run/have5.lean index ac9f727e9..6a04f24ab 100644 --- a/tests/lean/run/have5.lean +++ b/tests/lean/run/have5.lean @@ -1,6 +1,6 @@ import standard using tactic -variables a b c d : Bool +variables a b c d : Prop axiom Ha : a axiom Hb : b axiom Hc : c diff --git a/tests/lean/run/have6.lean b/tests/lean/run/have6.lean index b51e78d20..758bf68fd 100644 --- a/tests/lean/run/have6.lean +++ b/tests/lean/run/have6.lean @@ -1,8 +1,8 @@ -abbreviation Bool : Type.{1} := Type.{0} -variable and : Bool → Bool → Bool +abbreviation Prop : Type.{1} := Type.{0} +variable and : Prop → Prop → Prop infixl `∧`:25 := and -variable and_intro : forall (a b : Bool), a → b → a ∧ b -variables a b c d : Bool +variable and_intro : forall (a b : Prop), a → b → a ∧ b +variables a b c d : Prop axiom Ha : a axiom Hb : b axiom Hc : c diff --git a/tests/lean/run/id.lean b/tests/lean/run/id.lean index dc0fa0abc..05f1ba8d2 100644 --- a/tests/lean/run/id.lean +++ b/tests/lean/run/id.lean @@ -3,7 +3,7 @@ definition id {A : Type} (a : A) := a check id id set_option pp.universes true check id id -check id Bool +check id Prop check id num.num check @id.{0} check @id.{1} diff --git a/tests/lean/run/ind5.lean b/tests/lean/run/ind5.lean index ca6ace6c4..77a65d18b 100644 --- a/tests/lean/run/ind5.lean +++ b/tests/lean/run/ind5.lean @@ -1,6 +1,6 @@ -definition Bool [inline] : Type.{1} := Type.{0} +definition Prop [inline] : Type.{1} := Type.{0} -inductive or (A B : Bool) : Bool := +inductive or (A B : Prop) : Prop := | or_intro_left : A → or A B | or_intro_right : B → or A B diff --git a/tests/lean/run/induniv.lean b/tests/lean/run/induniv.lean index f710198bb..cdc542b25 100644 --- a/tests/lean/run/induniv.lean +++ b/tests/lean/run/induniv.lean @@ -32,13 +32,13 @@ section | mk_pair : A → B → pair end -definition Bool [inline] := Type.{0} -inductive eq {A : Type} (a : A) : A → Bool := +definition Prop [inline] := Type.{0} +inductive eq {A : Type} (a : A) : A → Prop := | refl : eq a a section parameter {A : Type} - inductive eq2 (a : A) : A → Bool := + inductive eq2 (a : A) : A → Prop := | refl2 : eq2 a a end diff --git a/tests/lean/run/is_nil.lean b/tests/lean/run/is_nil.lean index 9e39e9ee0..2a92db726 100644 --- a/tests/lean/run/is_nil.lean +++ b/tests/lean/run/is_nil.lean @@ -5,7 +5,7 @@ inductive list (A : Type) : Type := | nil {} : list A | cons : A → list A → list A -definition is_nil {A : Type} (l : list A) : Bool +definition is_nil {A : Type} (l : list A) : Prop := list_rec true (fun h t r, false) l theorem is_nil_nil (A : Type) : is_nil (@nil A) @@ -19,13 +19,13 @@ theorem cons_ne_nil {A : Type} (a : A) (l : list A) : ¬ cons a l = nil ... = false : refl _) true_ne_false) -theorem T : is_nil (@nil Bool) +theorem T : is_nil (@nil Prop) := by apply is_nil_nil (* -local list = Const("list", {1})(Bool) -local isNil = Const("is_nil", {1})(Bool) -local Nil = Const("nil", {1})(Bool) +local list = Const("list", {1})(Prop) +local isNil = Const("is_nil", {1})(Prop) +local Nil = Const("nil", {1})(Prop) local m = mk_metavar("m", list) print(isNil(Nil)) print(isNil(m)) diff --git a/tests/lean/run/n3.lean b/tests/lean/run/n3.lean index dd1741c66..8498d81fc 100644 --- a/tests/lean/run/n3.lean +++ b/tests/lean/run/n3.lean @@ -1,9 +1,9 @@ -definition Bool [inline] : Type.{1} := Type.{0} +definition Prop [inline] : Type.{1} := Type.{0} variable N : Type.{1} -variable and : Bool → Bool → Bool +variable and : Prop → Prop → Prop infixr `∧`:35 := and -variable le : N → N → Bool -variable lt : N → N → Bool +variable le : N → N → Prop +variable lt : N → N → Prop variable f : N → N variable add : N → N → N infixl `+`:65 := add diff --git a/tests/lean/run/n4.lean b/tests/lean/run/n4.lean index 04933b9c2..50093aae5 100644 --- a/tests/lean/run/n4.lean +++ b/tests/lean/run/n4.lean @@ -1,17 +1,17 @@ -definition Bool [inline] : Type.{1} := Type.{0} +definition Prop [inline] : Type.{1} := Type.{0} section variable N : Type.{1} variables a b c : N - variable and : Bool → Bool → Bool + variable and : Prop → Prop → Prop infixr `∧`:35 := and - variable le : N → N → Bool - variable lt : N → N → Bool + variable le : N → N → Prop + variable lt : N → N → Prop precedence `≤`:50 precedence `<`:50 infixl ≤ := le infixl < := lt check a ≤ b - definition T : Bool := a ≤ b + definition T : Prop := a ≤ b check T end check T diff --git a/tests/lean/run/root.lean b/tests/lean/run/root.lean index 6a033dd51..a28906a1f 100644 --- a/tests/lean/run/root.lean +++ b/tests/lean/run/root.lean @@ -1,14 +1,14 @@ import standard using num -variable foo : Bool +variable foo : Prop namespace N1 - variable foo : Bool + variable foo : Prop check N1.foo check _root_.foo namespace N2 - variable foo : Bool + variable foo : Prop check N1.foo check N1.N2.foo print raw foo diff --git a/tests/lean/run/simple.lean b/tests/lean/run/simple.lean index e2839e131..b56520927 100644 --- a/tests/lean/run/simple.lean +++ b/tests/lean/run/simple.lean @@ -1,15 +1,15 @@ -abbreviation Bool : Type.{1} := Type.{0} +abbreviation Prop : Type.{1} := Type.{0} section parameter A : Type - definition eq (a b : A) : Bool - := ∀P : A → Bool, P a → P b + definition eq (a b : A) : Prop + := ∀P : A → Prop, P a → P b - theorem subst (P : A → Bool) (a b : A) (H1 : eq a b) (H2 : P a) : P b + theorem subst (P : A → Prop) (a b : A) (H1 : eq a b) (H2 : P a) : P b := H1 P H2 theorem refl (a : A) : eq a a - := λ (P : A → Bool) (H : P a), H + := λ (P : A → Prop) (H : P a), H theorem symm (a b : A) (H : eq a b) : eq b a := subst (λ x : A, eq x a) a b H (refl a) diff --git a/tests/lean/run/t1.lean b/tests/lean/run/t1.lean index 56019b10f..9d2f3d674 100644 --- a/tests/lean/run/t1.lean +++ b/tests/lean/run/t1.lean @@ -1,9 +1,9 @@ -definition Bool : Type.{1} := Type.{0} -print raw ((Bool)) -print raw Bool -print raw fun (x y : Bool), x x -print raw fun (x y : Bool) {z : Bool}, x y -print raw λ [x y : Bool] {z : Bool}, x z -print raw Pi (x y : Bool) {z : Bool}, x -print raw ∀ (x y : Bool) {z : Bool}, x -print raw forall {x y : Bool} w {z : Bool}, x +definition Prop : Type.{1} := Type.{0} +print raw ((Prop)) +print raw Prop +print raw fun (x y : Prop), x x +print raw fun (x y : Prop) {z : Prop}, x y +print raw λ [x y : Prop] {z : Prop}, x z +print raw Pi (x y : Prop) {z : Prop}, x +print raw ∀ (x y : Prop) {z : Prop}, x +print raw forall {x y : Prop} w {z : Prop}, x diff --git a/tests/lean/run/tactic1.lean b/tests/lean/run/tactic1.lean index cf4729fa6..c7d76b472 100644 --- a/tests/lean/run/tactic1.lean +++ b/tests/lean/run/tactic1.lean @@ -1,5 +1,5 @@ import standard using tactic -theorem tst {A B : Bool} (H1 : A) (H2 : B) : A +theorem tst {A B : Prop} (H1 : A) (H2 : B) : A := by assumption diff --git a/tests/lean/run/tactic10.lean b/tests/lean/run/tactic10.lean index aa8caedaf..975686b87 100644 --- a/tests/lean/run/tactic10.lean +++ b/tests/lean/run/tactic10.lean @@ -1,7 +1,7 @@ import standard using tactic -theorem tst (a b : Bool) (H : a ↔ b) : b ↔ a +theorem tst (a b : Prop) (H : a ↔ b) : b ↔ a := by apply iff_intro; apply (assume Hb, iff_mp_right H Hb); apply (assume Ha, iff_mp_left H Ha) diff --git a/tests/lean/run/tactic11.lean b/tests/lean/run/tactic11.lean index bf570c438..0d1a6c865 100644 --- a/tests/lean/run/tactic11.lean +++ b/tests/lean/run/tactic11.lean @@ -1,7 +1,7 @@ import standard using tactic -theorem tst (a b : Bool) (H : a ↔ b) : b ↔ a +theorem tst (a b : Prop) (H : a ↔ b) : b ↔ a := have H1 [fact] : a → b, -- We need to mark H1 as fact, otherwise it is not visible by tactics from iff_elim_left H, by apply iff_intro; diff --git a/tests/lean/run/tactic12.lean b/tests/lean/run/tactic12.lean index 37db1fc8b..faf9ef85d 100644 --- a/tests/lean/run/tactic12.lean +++ b/tests/lean/run/tactic12.lean @@ -1,7 +1,7 @@ import standard using tactic -theorem tst (a b : Bool) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b +theorem tst (a b : Prop) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b := by apply and_intro; apply not_intro; exact diff --git a/tests/lean/run/tactic13.lean b/tests/lean/run/tactic13.lean index 58eff1fb5..23e47ace4 100644 --- a/tests/lean/run/tactic13.lean +++ b/tests/lean/run/tactic13.lean @@ -1,7 +1,7 @@ import standard using tactic -theorem tst (a b : Bool) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b := +theorem tst (a b : Prop) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b := proof apply and_intro, apply not_intro, diff --git a/tests/lean/run/tactic14.lean b/tests/lean/run/tactic14.lean index e1514e86b..304db5703 100644 --- a/tests/lean/run/tactic14.lean +++ b/tests/lean/run/tactic14.lean @@ -6,7 +6,7 @@ definition basic_tac : tactic set_proof_qed basic_tac -- basic_tac is automatically applied to each element of a proof-qed block -theorem tst (a b : Bool) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b := +theorem tst (a b : Prop) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b := proof assume Ha, or_elim H (assume Hna, absurd Ha Hna) diff --git a/tests/lean/run/tactic2.lean b/tests/lean/run/tactic2.lean index fd64eb64e..a554983d0 100644 --- a/tests/lean/run/tactic2.lean +++ b/tests/lean/run/tactic2.lean @@ -1,7 +1,7 @@ import standard using tactic -theorem tst {A B : Bool} (H1 : A) (H2 : B) : A +theorem tst {A B : Prop} (H1 : A) (H2 : B) : A := by state; assumption check tst \ No newline at end of file diff --git a/tests/lean/run/tactic21.lean b/tests/lean/run/tactic21.lean index 2e043c379..2f721b8c9 100644 --- a/tests/lean/run/tactic21.lean +++ b/tests/lean/run/tactic21.lean @@ -3,10 +3,10 @@ using tactic definition assump := eassumption -theorem tst1 {A : Type} {a b c : A} {p : A → A → Bool} (H1 : p a b) (H2 : p b c) : ∃ x, p a x ∧ p x c +theorem tst1 {A : Type} {a b c : A} {p : A → A → Prop} (H1 : p a b) (H2 : p b c) : ∃ x, p a x ∧ p x c := by apply exists_intro; apply and_intro; assump; assump -theorem tst2 {A : Type} {a b c d : A} {p : A → A → Bool} (Ha : p a c) (H1 : p a b) (Hb : p b d) (H2 : p b c) : ∃ x, p a x ∧ p x c +theorem tst2 {A : Type} {a b c d : A} {p : A → A → Prop} (Ha : p a c) (H1 : p a b) (Hb : p b d) (H2 : p b c) : ∃ x, p a x ∧ p x c := by apply exists_intro; apply and_intro; assump; assump (* diff --git a/tests/lean/run/tactic22.lean b/tests/lean/run/tactic22.lean index 6aed4e468..a6623c176 100644 --- a/tests/lean/run/tactic22.lean +++ b/tests/lean/run/tactic22.lean @@ -1,5 +1,5 @@ import standard using tactic -theorem T (a b c d : Bool) (Ha : a) (Hb : b) (Hc : c) (Hd : d) : a ∧ b ∧ c ∧ d +theorem T (a b c d : Prop) (Ha : a) (Hb : b) (Hc : c) (Hd : d) : a ∧ b ∧ c ∧ d := by fixpoint (λ f, [apply @and_intro; f | assumption; f | id]) diff --git a/tests/lean/run/tactic23.lean b/tests/lean/run/tactic23.lean index 4196816a3..7608169dd 100644 --- a/tests/lean/run/tactic23.lean +++ b/tests/lean/run/tactic23.lean @@ -26,7 +26,7 @@ check 2 + 3 -- Define an assump as an alias for the eassumption tactic definition assump : tactic := eassumption -theorem T1 {p : nat → Bool} {a : nat } (H : p (a+2)) : ∃ x, p (succ x) +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) diff --git a/tests/lean/run/tactic24.lean b/tests/lean/run/tactic24.lean index f9772bc2d..e7e60aa17 100644 --- a/tests/lean/run/tactic24.lean +++ b/tests/lean/run/tactic24.lean @@ -10,7 +10,7 @@ tactic_hint my_tac2 theorem T1 {A : Type.{2}} (a : A) : a = a := _ -theorem T2 {a b c : Bool} (Ha : a) (Hb : b) (Hc : c) : a ∧ b ∧ c +theorem T2 {a b c : Prop} (Ha : a) (Hb : b) (Hc : c) : a ∧ b ∧ c := _ definition my_tac3 := fixpoint (λ f, [apply @or_intro_left; f | @@ -19,5 +19,5 @@ definition my_tac3 := fixpoint (λ f, [apply @or_intro_left; f | tactic_hint [or] my_tac3 -theorem T3 {a b c : Bool} (Hb : b) : a ∨ b ∨ c +theorem T3 {a b c : Prop} (Hb : b) : a ∨ b ∨ c := _ diff --git a/tests/lean/run/tactic25.lean b/tests/lean/run/tactic25.lean index 6cbc7081c..5fa7c7205 100644 --- a/tests/lean/run/tactic25.lean +++ b/tests/lean/run/tactic25.lean @@ -9,11 +9,11 @@ tactic_hint my_tac2 theorem T1 {A : Type.{2}} (a : A) : a = a -theorem T2 {a b c : Bool} (Ha : a) (Hb : b) (Hc : c) : a ∧ b ∧ c +theorem T2 {a b c : Prop} (Ha : a) (Hb : b) (Hc : c) : a ∧ b ∧ c definition my_tac3 := fixpoint (λ f, [apply @or_intro_left; f | apply @or_intro_right; f | assumption]) tactic_hint [or] my_tac3 -theorem T3 {a b c : Bool} (Hb : b) : a ∨ b ∨ c +theorem T3 {a b c : Prop} (Hb : b) : a ∨ b ∨ c diff --git a/tests/lean/run/tactic3.lean b/tests/lean/run/tactic3.lean index 443e04abe..b3797c6e5 100644 --- a/tests/lean/run/tactic3.lean +++ b/tests/lean/run/tactic3.lean @@ -1,7 +1,7 @@ import standard using tactic -theorem tst {A B : Bool} (H1 : A) (H2 : B) : A +theorem tst {A B : Prop} (H1 : A) (H2 : B) : A := by [trace "first"; state; now | trace "second"; state; fail | trace "third"; assumption] diff --git a/tests/lean/run/tactic4.lean b/tests/lean/run/tactic4.lean index cda3ca020..98184be23 100644 --- a/tests/lean/run/tactic4.lean +++ b/tests/lean/run/tactic4.lean @@ -3,10 +3,10 @@ using tactic (renaming id->id_tac) definition id {A : Type} (a : A) := a -definition simple {A : Bool} : tactic +definition simple {A : Prop} : tactic := unfold @id.{1}; assumption -theorem tst {A B : Bool} (H1 : A) (H2 : B) : id A +theorem tst {A B : Prop} (H1 : A) (H2 : B) : id A := by simple check tst diff --git a/tests/lean/run/tactic5.lean b/tests/lean/run/tactic5.lean index b4b8f520c..123e494f9 100644 --- a/tests/lean/run/tactic5.lean +++ b/tests/lean/run/tactic5.lean @@ -3,7 +3,7 @@ using tactic (renaming id->id_tac) definition id {A : Type} (a : A) := a -theorem tst {A B : Bool} (H1 : A) (H2 : B) : id A +theorem tst {A B : Prop} (H1 : A) (H2 : B) : id A := by !(unfold @id; state); assumption check tst \ No newline at end of file diff --git a/tests/lean/run/tactic6.lean b/tests/lean/run/tactic6.lean index e111ed447..6ef178c48 100644 --- a/tests/lean/run/tactic6.lean +++ b/tests/lean/run/tactic6.lean @@ -3,7 +3,7 @@ using tactic (renaming id->id_tac) definition id {A : Type} (a : A) := a -theorem tst {A B : Bool} (H1 : A) (H2 : B) : id A +theorem tst {A B : Prop} (H1 : A) (H2 : B) : id A := by unfold id; assumption check tst diff --git a/tests/lean/run/tactic7.lean b/tests/lean/run/tactic7.lean index 2a2f43255..26f8042f1 100644 --- a/tests/lean/run/tactic7.lean +++ b/tests/lean/run/tactic7.lean @@ -1,11 +1,11 @@ import standard using tactic -theorem tst {A B : Bool} (H1 : A) (H2 : B) : A ∧ B ∧ A +theorem tst {A B : Prop} (H1 : A) (H2 : B) : A ∧ B ∧ A := by apply and_intro; state; assumption; apply and_intro; !assumption check tst -theorem tst2 {A B : Bool} (H1 : A) (H2 : B) : A ∧ B ∧ A +theorem tst2 {A B : Prop} (H1 : A) (H2 : B) : A ∧ B ∧ A := by !([apply @and_intro | assumption] ; trace "STEP"; state; trace "----------") check tst2 diff --git a/tests/lean/run/tactic8.lean b/tests/lean/run/tactic8.lean index aae365ab2..371b99bd1 100644 --- a/tests/lean/run/tactic8.lean +++ b/tests/lean/run/tactic8.lean @@ -1,7 +1,7 @@ import standard using tactic -theorem tst {A B : Bool} (H1 : A) (H2 : B) : A ∧ B ∧ A +theorem tst {A B : Prop} (H1 : A) (H2 : B) : A ∧ B ∧ A := by (apply @and_intro; apply (show A, from H1); apply (show B ∧ A, from and_intro H2 H1)) diff --git a/tests/lean/run/tactic9.lean b/tests/lean/run/tactic9.lean index 55d29d816..3cc5dea31 100644 --- a/tests/lean/run/tactic9.lean +++ b/tests/lean/run/tactic9.lean @@ -1,6 +1,6 @@ import standard using tactic -theorem tst {A B : Bool} (H1 : A) (H2 : B) : ((fun x : Bool, x) A) ∧ B ∧ A +theorem tst {A B : Prop} (H1 : A) (H2 : B) : ((fun x : Prop, x) A) ∧ B ∧ A := by apply and_intro; beta; assumption; apply and_intro; !assumption diff --git a/tests/lean/run/uni.lean b/tests/lean/run/uni.lean index 378842df0..f4fa23eae 100644 --- a/tests/lean/run/uni.lean +++ b/tests/lean/run/uni.lean @@ -11,8 +11,8 @@ local env = get_env() local nat_rec = Const("nat_rec", {1}) local nat = Const("nat") local n = Local("n", nat) -local C = Fun(n, Bool) -local p = Local("p", Bool) +local C = Fun(n, Prop) +local p = Local("p", Prop) local ff = Const("false") local tt = Const("true") local t = nat_rec(C, ff, Fun(n, p, tt)) diff --git a/tests/lean/run/uni2.lean b/tests/lean/run/uni2.lean index d0bf013f8..407b1a011 100644 --- a/tests/lean/run/uni2.lean +++ b/tests/lean/run/uni2.lean @@ -14,8 +14,8 @@ local nat_rec = Const("nat_rec", {1}) local nat = Const("nat") local f = Const("f") local n = Local("n", nat) -local C = Fun(n, Bool) -local p = Local("p", Bool) +local C = Fun(n, Prop) +local p = Local("p", Prop) local ff = Const("false") local tt = Const("true") local t = nat_rec(C, ff, Fun(n, p, tt)) diff --git a/tests/lean/t1.lean b/tests/lean/t1.lean index 5821d7a30..eb88fc206 100644 --- a/tests/lean/t1.lean +++ b/tests/lean/t1.lean @@ -2,7 +2,7 @@ (* print("testing...") local env = get_env() -env = add_decl(env, mk_var_decl("x", Bool)) +env = add_decl(env, mk_var_decl("x", Prop)) assert(env:find("x")) set_env(env) *) diff --git a/tests/lean/t1.lean.expected.out b/tests/lean/t1.lean.expected.out index 3f13e2241..717d8562e 100644 --- a/tests/lean/t1.lean.expected.out +++ b/tests/lean/t1.lean.expected.out @@ -1,2 +1,2 @@ testing... -Bool +Prop diff --git a/tests/lean/t4.lean b/tests/lean/t4.lean index 9118bf0de..a053e49d1 100644 --- a/tests/lean/t4.lean +++ b/tests/lean/t4.lean @@ -1,9 +1,9 @@ -definition Bool [inline] : Type.{1} := Type.{0} +definition Prop [inline] : Type.{1} := Type.{0} variable N : Type.{1} check N variable a : N check a -check Bool → Bool +check Prop → Prop variable F.{l} : Type.{l} → Type.{l} check F.{2} universe u @@ -15,7 +15,7 @@ check f check len.{1} section variable A : Type - variable B : Bool + variable B : Prop hypothesis H : B parameter {C : Type} check B -> B diff --git a/tests/lean/t4.lean.expected.out b/tests/lean/t4.lean.expected.out index 3fc13ad66..4b66b07bf 100644 --- a/tests/lean/t4.lean.expected.out +++ b/tests/lean/t4.lean.expected.out @@ -1,15 +1,15 @@ N : Type a : N -Bool → Bool : Type +Prop → Prop : Type F : Type → Type F : Type → Type f : N → N → N len : Π (A : Type) (n : N), vec A n → N -B → B : Bool +B → B : Prop A → A : Type C : Type t4.lean:25:6: error: unknown identifier 'A' -R : Type → Bool +R : Type → Prop λ (x y : N), x : N → N → N [choice N N] N @@ -30,6 +30,6 @@ R len vec f +Prop foo.M -Bool ------------- diff --git a/tests/lean/t6.lean b/tests/lean/t6.lean index 40bb5b2f9..53a5e5bc8 100644 --- a/tests/lean/t6.lean +++ b/tests/lean/t6.lean @@ -1,10 +1,10 @@ -definition Bool : Type.{1} := Type.{0} +definition Prop : Type.{1} := Type.{0} section parameter {A : Type} -- Mark A as implicit parameter - parameter R : A → A → Bool + parameter R : A → A → Prop definition id (a : A) : A := a - definition refl : Bool := forall (a : A), R a a - definition symm : Bool := forall (a b : A), R a b -> R b a + definition refl : Prop := forall (a : A), R a a + definition symm : Prop := forall (a b : A), R a b -> R b a end check id.{2} check refl.{1} diff --git a/tests/lean/t6.lean.expected.out b/tests/lean/t6.lean.expected.out index 335ec2e2c..cf7d444a0 100644 --- a/tests/lean/t6.lean.expected.out +++ b/tests/lean/t6.lean.expected.out @@ -1,3 +1,3 @@ id : ?M_1 → ?M_1 -refl : (?M_1 → ?M_1 → Bool) → Bool -symm : (?M_1 → ?M_1 → Bool) → Bool +refl : (?M_1 → ?M_1 → Prop) → Prop +symm : (?M_1 → ?M_1 → Prop) → Prop diff --git a/tests/lean/t7.lean b/tests/lean/t7.lean index 3a440c6de..972b28f62 100644 --- a/tests/lean/t7.lean +++ b/tests/lean/t7.lean @@ -1,14 +1,14 @@ -definition Bool : Type.{1} := Type.{0} -variable and : Bool → Bool → Bool +definition Prop : Type.{1} := Type.{0} +variable and : Prop → Prop → Prop section parameter {A : Type} -- Mark A as implicit parameter - parameter R : A → A → Bool + parameter R : A → A → Prop parameter B : Type definition id (a : A) : A := a - definition refl [private] : Bool := ∀ (a : A), R a a - definition symm : Bool := ∀ (a b : A), R a b → R b a - definition trans : Bool := ∀ (a b c : A), R a b → R b c → R a c - definition equivalence : Bool := and (and refl symm) trans + definition refl [private] : Prop := ∀ (a : A), R a a + definition symm : Prop := ∀ (a b : A), R a b → R b a + definition trans : Prop := ∀ (a b c : A), R a b → R b c → R a c + definition equivalence : Prop := and (and refl symm) trans end check id.{2} check trans.{1} diff --git a/tests/lean/t7.lean.expected.out b/tests/lean/t7.lean.expected.out index ff853a034..022fc6d0b 100644 --- a/tests/lean/t7.lean.expected.out +++ b/tests/lean/t7.lean.expected.out @@ -1,6 +1,6 @@ id : ?M_1 → ?M_1 -trans : (?M_1 → ?M_1 → Bool) → Bool -symm : (?M_1 → ?M_1 → Bool) → Bool -equivalence : (?M_1 → ?M_1 → Bool) → Bool -λ (A : Type) (R : A → A → Bool), +trans : (?M_1 → ?M_1 → Prop) → Prop +symm : (?M_1 → ?M_1 → Prop) → Prop +equivalence : (?M_1 → ?M_1 → Prop) → Prop +λ (A : Type) (R : A → A → Prop), and (and (refl R) (symm R)) (trans R) diff --git a/tests/lua/ac.lua b/tests/lua/ac.lua index 51b902384..e236050ec 100644 --- a/tests/lua/ac.lua +++ b/tests/lua/ac.lua @@ -2,12 +2,12 @@ local env = environment() local l = param_univ("l") local U_l = mk_sort(l) local A = Local("A", U_l) -local R = Local("R", mk_arrow(A, A, Bool)) +local R = Local("R", mk_arrow(A, A, Prop)) local Acc = Const("Acc", {l}) local x = Local("x", A) local y = Local("y", A) env = add_inductive(env, - "Acc", {l}, 2, Pi(A, R, x, Bool), + "Acc", {l}, 2, Pi(A, R, x, Prop), "Acc_intro", Pi(A, R, x, mk_arrow(Pi(y, mk_arrow(R(y, x), Acc(A, R, y))), Acc(A, R, x)))) function display_type(env, t) diff --git a/tests/lua/acc.lua b/tests/lua/acc.lua index baed71fb4..5b0fca43a 100644 --- a/tests/lua/acc.lua +++ b/tests/lua/acc.lua @@ -7,7 +7,7 @@ local env = environment() local l = param_univ("l") local U_l = mk_sort(l) local A = Local("A", U_l) -local R = Local("R", mk_arrow(A, A, Bool)) +local R = Local("R", mk_arrow(A, A, Prop)) local x = Local("x", A) local y = Local("y", A) local Acc = Const("Acc", {l}) @@ -24,7 +24,7 @@ display_type(env, Const("Acc_rec", {v, u})) -- well_founded_induction_type : -- Pi (A : Type) --- (R : A -> A -> Bool) +-- (R : A -> A -> Prop) -- (R_is_wf : Pi (a : A), (Acc A R a)) -- (P : A -> Type) -- (H : Pi (x : A) (Hr : Pi (y : A) (a : R y x), (P y)), (P x)) @@ -36,7 +36,7 @@ local Acc = Const("Acc", {l1}) local Acc_intro = Const("Acc_intro", {l1}) local Acc_rec = Const("Acc_rec", {l2, l1}) local A = Local("A", mk_sort(l1)) -local R = Local("R", mk_arrow(A, A, Bool)) +local R = Local("R", mk_arrow(A, A, Prop)) local x = Local("x", A) local y = Local("y", A) local a = Local("a", A) diff --git a/tests/lua/alias1.lua b/tests/lua/alias1.lua index 09ac0850c..447e667d7 100644 --- a/tests/lua/alias1.lua +++ b/tests/lua/alias1.lua @@ -3,7 +3,7 @@ local env = environment() local env = environment() local l = mk_param_univ("l") local U_l = mk_sort(l) -local U_l1 = mk_sort(max_univ(l, 1)) -- Make sure U_l1 is not Bool/Prop +local U_l1 = mk_sort(max_univ(l, 1)) -- Make sure U_l1 is not Prop local nat = Const({"nat", "nat"}) local vec_l = Const({"vec", "vec"}, {l}) -- vec.{l} local zero = Const({"nat", "zero"}) @@ -41,7 +41,7 @@ print(get_alias_exprs(env, {"l", "list"}):head()) print(get_alias_exprs(env, {"l", "cons"}):head()) local A = Local("A", mk_sort(1)) -local R = Local("R", mk_arrow(A, A, Bool)) +local R = Local("R", mk_arrow(A, A, Prop)) local a = Local("a", A) local b = Local("b", A) diff --git a/tests/lua/alias3.lua b/tests/lua/alias3.lua index 3573b97de..9d8b5c080 100644 --- a/tests/lua/alias3.lua +++ b/tests/lua/alias3.lua @@ -1,7 +1,7 @@ local env = environment() -env = add_decl(env, mk_var_decl(name("foo", "x"), Bool)) -env = add_decl(env, mk_var_decl(name("foo", "y"), Bool)) -env = add_decl(env, mk_var_decl(name("foo", "z"), Bool)) +env = add_decl(env, mk_var_decl(name("foo", "x"), Prop)) +env = add_decl(env, mk_var_decl(name("foo", "y"), Prop)) +env = add_decl(env, mk_var_decl(name("foo", "z"), Prop)) env = env:add_universe(name("foo", "u")) env = env:add_universe(name("foo", "v")) env = add_aliases(env, "foo", "bla", {"z", "v"}) diff --git a/tests/lua/choice2.lua b/tests/lua/choice2.lua index 332e4ced9..138483e5f 100644 --- a/tests/lua/choice2.lua +++ b/tests/lua/choice2.lua @@ -1,5 +1,5 @@ -local a = Local("a", Bool) -local b = Local("b", Bool) +local a = Local("a", Prop) +local b = Local("b", Prop) local c = mk_choice(a, b) print(c) local env = environment() diff --git a/tests/lua/cnstr1.lua b/tests/lua/cnstr1.lua index e84d34699..5591d33a5 100644 --- a/tests/lua/cnstr1.lua +++ b/tests/lua/cnstr1.lua @@ -1,6 +1,6 @@ local a = Const("a") local f = Const("f") -local m = mk_metavar("m", Bool) +local m = mk_metavar("m", Prop) local j = justification("type match") local c = mk_eq_cnstr(f(a), m, j) assert(c:is_eq()) diff --git a/tests/lua/def1.lua b/tests/lua/def1.lua index f00d810c5..915684bc0 100644 --- a/tests/lua/def1.lua +++ b/tests/lua/def1.lua @@ -42,9 +42,9 @@ assert(d3:weight() == 100) assert(d3:module_idx() == 10) assert(not d3:use_conv_opt()) local env = bare_environment() -local d4 = mk_definition(env, "bool", Type, Bool) +local d4 = mk_definition(env, "bool", Type, Prop) assert(d4:weight() == 1) -local d5 = mk_definition(env, "bool", Type, Bool, {opaque=false, weight=100, module_idx=3, use_conv_opt=true}) +local d5 = mk_definition(env, "bool", Type, Prop, {opaque=false, weight=100, module_idx=3, use_conv_opt=true}) assert(not d5:opaque()) assert(d5:weight() == 1) assert(d5:module_idx() == 3) diff --git a/tests/lua/env11.lua b/tests/lua/env11.lua index e30efb2bc..dcf55529c 100644 --- a/tests/lua/env11.lua +++ b/tests/lua/env11.lua @@ -1,8 +1,8 @@ local A = Const("A") local B = Const("B") local env = environment() -local env1 = add_decl(env, mk_var_decl("A", Bool)) -env1 = add_decl(env1, mk_var_decl("B", Bool)) +local env1 = add_decl(env, mk_var_decl("A", Prop)) +env1 = add_decl(env1, mk_var_decl("B", Prop)) env1 = add_decl(env1, mk_axiom("H", B)) local c1 = check(env1, mk_axiom("H1", A)) local c2 = check(env1, mk_axiom("H2", A)) @@ -28,7 +28,7 @@ assert(not env3:find("H2"):is_axiom()) assert(env3:find("H2"):is_theorem()) local c5 = check(env1b, mk_theorem("H5", A, Const("H1"))) expected_error(function() env3:replace(c5) end) -local c6 = check(env, mk_definition("A", Type, Bool)) +local c6 = check(env, mk_definition("A", Type, Prop)) expected_error(function() env3:replace(c6) end) local c7 = check(env1b, mk_definition("H2", A, Const("H1"))) expected_error(function() env2:replace(c7) end) diff --git a/tests/lua/env3.lua b/tests/lua/env3.lua index fbe3c9493..4429ade4a 100644 --- a/tests/lua/env3.lua +++ b/tests/lua/env3.lua @@ -1,6 +1,6 @@ function init(env) - env = add_decl(env, mk_var_decl("A", Bool)) - env = add_decl(env, mk_var_decl("And", mk_arrow(Bool, mk_arrow(Bool, Bool)))) + env = add_decl(env, mk_var_decl("A", Prop)) + env = add_decl(env, mk_var_decl("And", mk_arrow(Prop, mk_arrow(Prop, Prop)))) env = add_decl(env, mk_axiom("p", Const("A"))) env = add_decl(env, mk_axiom("q", Const("A"))) return env diff --git a/tests/lua/env4.lua b/tests/lua/env4.lua index 475b7466a..3a58a96e8 100644 --- a/tests/lua/env4.lua +++ b/tests/lua/env4.lua @@ -1,5 +1,5 @@ local env = bare_environment() -env = add_decl(env, mk_var_decl("A", Bool)) +env = add_decl(env, mk_var_decl("A", Prop)) local c1 = type_check(env, mk_axiom("p", Const("A"))) local c2 = type_check(env, mk_axiom("q", Const("A"))) env = env:add(c1) diff --git a/tests/lua/env6.lua b/tests/lua/env6.lua index 2458e170f..4cddf098f 100644 --- a/tests/lua/env6.lua +++ b/tests/lua/env6.lua @@ -1,7 +1,7 @@ local env = bare_environment() -env = add_decl(env, mk_var_decl("A", Bool)) +env = add_decl(env, mk_var_decl("A", Prop)) local A = Const("A") -local x = Local("x", Bool) +local x = Local("x", Prop) env = add_decl(env, mk_axiom("magic", Pi(x, x))) local saved_env = env env = add_decl(env, mk_axiom("Ax", A)) diff --git a/tests/lua/env9.lua b/tests/lua/env9.lua index 50397989e..44db7894f 100644 --- a/tests/lua/env9.lua +++ b/tests/lua/env9.lua @@ -1,12 +1,12 @@ local env = bare_environment() -- Trust level is set to 0 by default. Then, we must type check a -- definition, before adding it to the environment -assert(not pcall(function() env:add(mk_var_decl("A", Bool)) end)) +assert(not pcall(function() env:add(mk_var_decl("A", Prop)) end)) -- The function check produces a "certified declaration". -env:add(check(env, mk_var_decl("A", Bool))) +env:add(check(env, mk_var_decl("A", Prop))) local env = bare_environment({trust_level = 10000000}) -- Now, env has trust_level > LEAN_BELIEVER_TRUST_LEVEL, then we can -- add declarations without type checking them. -env:add(mk_var_decl("A", Bool)) +env:add(mk_var_decl("A", Prop)) diff --git a/tests/lua/eta.lua b/tests/lua/eta.lua index 46bfe92a8..c553f70c5 100644 --- a/tests/lua/eta.lua +++ b/tests/lua/eta.lua @@ -1,9 +1,9 @@ local env = bare_environment() -env = add_decl(env, mk_var_decl("f", mk_arrow(Bool, mk_arrow(Bool, Bool)))) +env = add_decl(env, mk_var_decl("f", mk_arrow(Prop, mk_arrow(Prop, Prop)))) local f = Const("f") -local x = Local("x", Bool) -local y = Local("y", Bool) -local z = Local("z", Bool) +local x = Local("x", Prop) +local y = Local("y", Prop) +local z = Local("z", Prop) local tc = type_checker(env) print(tc:whnf(Fun(x, f(x)))) print(tc:whnf(Fun(x, y, f(x, y)))) diff --git a/tests/lua/expr10.lua b/tests/lua/expr10.lua index 9058c387c..4e6879bf8 100644 --- a/tests/lua/expr10.lua +++ b/tests/lua/expr10.lua @@ -1,8 +1,8 @@ local env = environment() -local f = Local("f", mk_arrow(Bool, Bool, Bool)) -local a = Local("a", Bool) -local b = Local("b", Bool) -local x = Local("x", Bool) +local f = Local("f", mk_arrow(Prop, Prop, Prop)) +local a = Local("a", Prop) +local b = Local("b", Prop) +local x = Local("x", Prop) local t = Fun(f, a, b, f(Fun(x, x)(b), a)) print(env:normalize(t)) assert(env:normalize(t) == Fun(f, a, b, f(b, a))) diff --git a/tests/lua/expr2.lua b/tests/lua/expr2.lua index d951e7d23..2ca54ebfc 100644 --- a/tests/lua/expr2.lua +++ b/tests/lua/expr2.lua @@ -6,15 +6,15 @@ assert(f(a, a):is_lt(f(a, b))) assert(Const("a"):is_lt(Const("b"))) assert(Var(0):is_lt(Const("b"))) assert(name("a") < name("b")) -assert(not (Bool:is_lt(Bool))) -assert(not (Bool < Bool)) -assert(mk_metavar("a", Bool):is_lt(mk_metavar("b", Bool))) -assert(not mk_metavar("a", Bool):is_lt(mk_metavar("a", Bool))) -assert(mk_metavar("a", Bool):is_lt(mk_metavar("a", Type))) -assert(mk_local("a", Bool):is_lt(mk_local("b", Bool))) -assert(not mk_local("a", Bool):is_lt(mk_local("a", Bool))) -assert(Bool:is_lt(Const("a"))) -local a = Local("a", Bool) +assert(not (Prop:is_lt(Prop))) +assert(not (Prop < Prop)) +assert(mk_metavar("a", Prop):is_lt(mk_metavar("b", Prop))) +assert(not mk_metavar("a", Prop):is_lt(mk_metavar("a", Prop))) +assert(mk_metavar("a", Prop):is_lt(mk_metavar("a", Type))) +assert(mk_local("a", Prop):is_lt(mk_local("b", Prop))) +assert(not mk_local("a", Prop):is_lt(mk_local("a", Prop))) +assert(Prop:is_lt(Const("a"))) +local a = Local("a", Prop) local a1 = Local("a1", Type) assert(Fun(a, a):is_lt(Fun(a1, a1))) assert(Fun(a, a):is_lt(Fun(a, Var(2)))) diff --git a/tests/lua/expr3.lua b/tests/lua/expr3.lua index c88116a26..245388455 100644 --- a/tests/lua/expr3.lua +++ b/tests/lua/expr3.lua @@ -9,30 +9,30 @@ assert(t:fn() == f) assert(t:arg() == a) assert(not pcall(function() f:fn() end)) -local a1 = Local("a", Bool) +local a1 = Local("a", Prop) local pi1 = Pi(a1, Type) assert(pi1:is_pi()) assert(not pcall(function() f:binding_name() end)) -local pi2 = mk_pi("a", Bool, Type, binder_info(true, true)) -local pi3 = mk_pi("a", Bool, Type) +local pi2 = mk_pi("a", Prop, Type, binder_info(true, true)) +local pi3 = mk_pi("a", Prop, Type) assert(pi2:binding_info():is_implicit()) assert(not pi3:binding_info():is_implicit()) -local l1 = mk_lambda("a", Bool, Var(0)) -local l2 = mk_lambda("a", Bool, Var(0), binder_info(true, false)) +local l1 = mk_lambda("a", Prop, Var(0)) +local l2 = mk_lambda("a", Prop, Var(0), binder_info(true, false)) assert(not l1:binding_info():is_implicit()) assert(l2:binding_info():is_implicit()) -local a = Local("a", Bool) -local b = Local("b", Bool) +local a = Local("a", Prop) +local b = Local("b", Prop) local pi3 = Pi(a, b, a) print(pi3) assert(not pcall(function() Pi(a) end)) local pi4 = Pi(a, b, a) print(pi4) assert(pi4:binding_name() == name("a")) -assert(pi4:binding_domain() == Bool) +assert(pi4:binding_domain() == Prop) assert(pi4:binding_body():is_pi()) @@ -46,16 +46,16 @@ assert(l1:is_lambda()) assert(pi3:is_pi()) assert(l1:is_binding()) assert(pi3:is_binding()) -assert(mk_metavar("m", Bool):is_metavar()) -assert(mk_local("m", Bool):is_local()) -assert(mk_metavar("m", Bool):is_mlocal()) -assert(mk_local("m", Bool):is_mlocal()) -assert(mk_metavar("m", Bool):is_meta()) -assert(mk_metavar("m", Bool)(a):is_meta()) -assert(f(mk_metavar("m", Bool)):has_metavar()) -assert(f(mk_local("l", Bool)):has_local()) -assert(not f(mk_metavar("m", Bool)):has_local()) -assert(not f(mk_local("l", Bool)):has_metavar()) +assert(mk_metavar("m", Prop):is_metavar()) +assert(mk_local("m", Prop):is_local()) +assert(mk_metavar("m", Prop):is_mlocal()) +assert(mk_local("m", Prop):is_mlocal()) +assert(mk_metavar("m", Prop):is_meta()) +assert(mk_metavar("m", Prop)(a):is_meta()) +assert(f(mk_metavar("m", Prop)):has_metavar()) +assert(f(mk_local("l", Prop)):has_local()) +assert(not f(mk_metavar("m", Prop)):has_local()) +assert(not f(mk_local("l", Prop)):has_metavar()) assert(f(mk_sort(mk_param_univ("l"))):has_param_univ()) assert(f(Var(0)):has_free_vars()) assert(not f(Var(0)):closed()) @@ -67,15 +67,15 @@ assert(mk_sort(mk_param_univ("l")):data() == mk_param_univ("l")) local f1, a1 = f(a):data() assert(f1 == f) assert(a1 == a) -local m1, t1 = mk_metavar("a", Bool):data() +local m1, t1 = mk_metavar("a", Prop):data() assert(m1 == name("a")) -assert(t1 == Bool) -local m1, t1 = mk_local("a", Bool):data() +assert(t1 == Prop) +local m1, t1 = mk_local("a", Prop):data() assert(m1 == name("a")) -assert(t1 == Bool) -local a1, t, b1, bi = mk_pi("a", Bool, Var(0), binder_info(true)):data() +assert(t1 == Prop) +local a1, t, b1, bi = mk_pi("a", Prop, Var(0), binder_info(true)):data() assert(a1 == name("a")) -assert(t == Bool) +assert(t == Prop) assert(b1 == Var(0)) assert(bi:is_implicit()) assert(not bi:is_cast()) diff --git a/tests/lua/expr9.lua b/tests/lua/expr9.lua index 2f7ddda0e..d30b66491 100644 --- a/tests/lua/expr9.lua +++ b/tests/lua/expr9.lua @@ -1,9 +1,9 @@ local env = environment() -local m = mk_metavar("m", mk_arrow(Bool, Bool)) -local a = Local("a", Bool) +local m = mk_metavar("m", mk_arrow(Prop, Prop)) +local a = Local("a", Prop) print(env:normalize(Fun(a, m))) print(env:normalize(Fun(a, m(a)))) -local m2 = mk_metavar("m2", mk_arrow(Bool, Bool, Bool)) +local m2 = mk_metavar("m2", mk_arrow(Prop, Prop, Prop)) print(env:normalize(Fun(a, (m2(a))(a)))) print("step1") env:type_check(m) diff --git a/tests/lua/goal1.lua b/tests/lua/goal1.lua index 6fe524772..f428d13d4 100644 --- a/tests/lua/goal1.lua +++ b/tests/lua/goal1.lua @@ -1,6 +1,6 @@ local env = environment() local A = Local("A", Type) -env = add_decl(env, mk_var_decl("eq", Pi(A, mk_arrow(A, A, Bool)))) +env = add_decl(env, mk_var_decl("eq", Pi(A, mk_arrow(A, A, Prop)))) local eq = Const("eq") local a = Local("a", A) local b = Local("b", A) @@ -11,6 +11,6 @@ print(m) print(env:type_check(m)) local g = goal(m, t) assert(g:validate(env)) -local m1 = g:mk_meta("m1", Bool) +local m1 = g:mk_meta("m1", Prop) print(tostring(m1)) print(env:type_check(m1)) diff --git a/tests/lua/ind1.lua b/tests/lua/ind1.lua index 01cd610da..05728f346 100644 --- a/tests/lua/ind1.lua +++ b/tests/lua/ind1.lua @@ -2,7 +2,7 @@ local env = environment() local l = mk_param_univ("l") local U_l = mk_sort(l) local A = Local("A", U_l) -local U_l1 = mk_sort(max_univ(l, 1)) -- Make sure U_l1 is not Bool/Prop +local U_l1 = mk_sort(max_univ(l, 1)) -- Make sure U_l1 is not Prop local list_l = Const("list", {l}) -- list.{l} local Nat = Const("nat") local vec_l = Const("vec", {l}) -- vec.{l} @@ -27,7 +27,7 @@ env = add_inductive(env, "succ", mk_arrow(Nat, Nat)) -- In the following inductive datatype, {l} is the list of universe level parameters. -- 1 is the number of parameters. --- The Boolean true in {A, U_l, true} is marking that this argument is implicit. +-- The Propean true in {A, U_l, true} is marking that this argument is implicit. env = add_inductive(env, "list", {l}, 1, Pi(A, U_l1), "nil", Pi(A, list_l(A)), @@ -40,24 +40,24 @@ env = add_inductive(env, local And = Const("and") local Or = Const("or") -- Datatype without introduction rules (aka constructors). It is a uninhabited type. -env = add_inductive(env, "false", Bool) +env = add_inductive(env, "false", Prop) -- Datatype with a single constructor. -env = add_inductive(env, "true", Bool, "trivial", Const("true")) -local A = Local("A", Bool) -local B = Local("B", Bool) +env = add_inductive(env, "true", Prop, "trivial", Const("true")) +local A = Local("A", Prop) +local B = Local("B", Prop) env = add_inductive(env, - "and", 2, Pi(A, B, Bool), + "and", 2, Pi(A, B, Prop), "and_intro", Pi(A, B, mk_arrow(A, B, And(A, B)))) env = add_inductive(env, - "or", 2, Pi(A, B, Bool), + "or", 2, Pi(A, B, Prop), "or_intro_left", Pi(A, B, mk_arrow(A, Or(A, B))), "or_intro_right", Pi(A, B, mk_arrow(B, Or(A, B)))) local A = Local("A", U_l) -local P = Local("P", mk_arrow(A, Bool)) +local P = Local("P", mk_arrow(A, Prop)) local a = Local("a", A) local exists_l = Const("exists", {l}) env = add_inductive(env, - "exists", {l}, 2, Pi(A, P, Bool), + "exists", {l}, 2, Pi(A, P, Prop), "exists_intro", Pi(A, P, a, mk_arrow(P(a), exists_l(A, P)))) env = add_inductive(env, {l}, 1, @@ -80,17 +80,17 @@ local Even = Const("Even") local Odd = Const("Odd") local b = Local("b", Nat) env = add_inductive(env, {}, - {"Even", mk_arrow(Nat, Bool), + {"Even", mk_arrow(Nat, Prop), "zero_is_even", Even(zero), "succ_odd", Pi(b, mk_arrow(Odd(b), Even(succ(b))))}, - {"Odd", mk_arrow(Nat, Bool), + {"Odd", mk_arrow(Nat, Prop), "succ_even", Pi(b, mk_arrow(Even(b), Odd(succ(b))))}) local flist_l = Const("flist", {l}) env = add_inductive(env, "flist", {l}, 1, Pi(A, U_l1), "fnil", Pi(A, flist_l(A)), - "fcons", Pi(A, mk_arrow(mk_arrow(Nat, A), mk_arrow(Nat, Bool, flist_l(A)), flist_l(A)))) + "fcons", Pi(A, mk_arrow(mk_arrow(Nat, A), mk_arrow(Nat, Prop, flist_l(A)), flist_l(A)))) local eq_l = Const("eq", {l}) @@ -98,7 +98,7 @@ local A = Local("A", U_l) local a = Local("a", A) local b = Local("b", A) env = add_inductive(env, - "eq", {l}, 2, Pi(A, a, b, Bool), + "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})) diff --git a/tests/lua/ind2.lua b/tests/lua/ind2.lua index ba914b5c0..76e219c67 100644 --- a/tests/lua/ind2.lua +++ b/tests/lua/ind2.lua @@ -9,7 +9,7 @@ end local l = mk_param_univ("l") local U_l = mk_sort(l) -local U_l1 = mk_sort(max_univ(l, 1)) -- Make sure U_l1 is not Bool/Prop +local U_l1 = mk_sort(max_univ(l, 1)) -- Make sure U_l1 is not Prop local list_l = Const("list", {l}) -- list.{l} local Nat = Const("nat") local vec_l = Const("vec", {l}) -- vec.{l} @@ -21,7 +21,7 @@ local n = Const("n") bad_add_inductive(env, "nat", Type, - "zero", Bool, -- Incorrect result type + "zero", Prop, -- Incorrect result type "succ", mk_arrow(Nat, Nat)) local A = Local("A", U_l) @@ -59,12 +59,12 @@ bad_add_inductive(env, {}, {"Even", mk_arrow(Nat, Type), "zero_is_even", Even(zero), "succ_odd", Pi(b, mk_arrow(Odd(b), Even(succ(b))))}, - {"Odd", mk_arrow(Nat, Bool), -- if one datatype lives in Bool/Prop, then all must live in Bool/Prop + {"Odd", mk_arrow(Nat, Prop), -- if one datatype lives in Prop, then all must live in Prop "succ_even", Pi(b, mk_arrow(Even(b), Odd(succ(b))))}) bad_add_inductive(env, "list", {l}, 1, mk_arrow(U_l, U_l1), - "nil", Pi(A, mk_arrow(mk_arrow(list_l(A), Bool), list_l(A))), -- nonpositive occurrence of inductive datatype + "nil", Pi(A, mk_arrow(mk_arrow(list_l(A), Prop), list_l(A))), -- nonpositive occurrence of inductive datatype "cons", Pi(A, mk_arrow(A, list_l(A), list_l(A)))) bad_add_inductive(env, @@ -95,7 +95,7 @@ bad_add_inductive(env, "cons", Pi(A, mk_arrow(list_l(A), A, list_l(A)))) local A = Local("A", Type) -env = add_decl(env, mk_var_decl("eq", Pi(A, mk_arrow(A, A, Bool)))) +env = add_decl(env, mk_var_decl("eq", Pi(A, mk_arrow(A, A, Prop)))) local eq = Const("eq") local Nat2 = Const("nat2") local a = Local("a", Nat2) diff --git a/tests/lua/ind4.lua b/tests/lua/ind4.lua index 534ee9f21..6a37b9969 100644 --- a/tests/lua/ind4.lua +++ b/tests/lua/ind4.lua @@ -5,7 +5,7 @@ end local env = environment() local l = param_univ("l") local U_l = mk_sort(l) -local U_l1 = mk_sort(max_univ(l, 1)) -- Make sure U_l1 is not Bool/Prop +local U_l1 = mk_sort(max_univ(l, 1)) -- Make sure U_l1 is not Prop local A = Local("A", U_l) local list_l = Const("list", {l}) diff --git a/tests/lua/ind5.lua b/tests/lua/ind5.lua index f6760deef..210acefa7 100644 --- a/tests/lua/ind5.lua +++ b/tests/lua/ind5.lua @@ -2,22 +2,22 @@ function display_type(env, t) print(tostring(t) .. " : " .. tostring(env:normalize(env:type_check(t)))) end -local A = Local("A", Bool) +local A = Local("A", Prop) local env = environment() local retraction = Const("retraction") env = add_inductive(env, - "retraction", Bool, + "retraction", Prop, "inj", Pi(A, retraction)) local u = global_univ("u") env = env:add_universe("u") -local a = Local("a", Bool) +local a = Local("a", Prop) local r = Local("r", retraction) local rec = Const("retraction_rec") display_type(env, rec) -local proj = Fun(r, rec(Bool, Fun(a, a), r)) +local proj = Fun(r, rec(Prop, Fun(a, a), r)) local inj = Const("inj") assert(not pcall(function() display_type(env, Fun(a, proj(inj(a)))) end)) diff --git a/tests/lua/ind_ex.lua b/tests/lua/ind_ex.lua index 3cccf6964..f932c0f9a 100644 --- a/tests/lua/ind_ex.lua +++ b/tests/lua/ind_ex.lua @@ -6,7 +6,7 @@ local A = Local("A", U_l) local a = Local("a", A) env = add_inductive(env, - "inhabited", {l}, 1, mk_arrow(U_l, Bool), + "inhabited", {l}, 1, mk_arrow(U_l, Prop), "inhabited_intro", Pi(A, a, inhabited(A))) function display_type(env, t) diff --git a/tests/lua/ind_tricky.lua b/tests/lua/ind_tricky.lua index 51fae1d89..1b3b563a5 100644 --- a/tests/lua/ind_tricky.lua +++ b/tests/lua/ind_tricky.lua @@ -1,10 +1,10 @@ local env = environment() local tricky = Const("tricky") -local P = Local("P", Bool) +local P = Local("P", Prop) env = add_inductive(env, - "tricky", Bool, + "tricky", Prop, "C", mk_arrow(Pi(P, mk_arrow(P, P)), tricky)) function display_type(env, t) diff --git a/tests/lua/jst1.lua b/tests/lua/jst1.lua index e332adb16..34de22934 100644 --- a/tests/lua/jst1.lua +++ b/tests/lua/jst1.lua @@ -8,7 +8,7 @@ local a = Const("a") local j1 = justification("expression must be a type", env, f(f(a))) assert(j1:is_asserted()) print(j1:pp()) -local m = mk_metavar("m", Bool) +local m = mk_metavar("m", Prop) local j2 = justification("expresion must be a Proposition", env, g(m)) print(j2:pp()) local s = substitution() diff --git a/tests/lua/mod1.lua b/tests/lua/mod1.lua index 12976da64..900b84e8b 100644 --- a/tests/lua/mod1.lua +++ b/tests/lua/mod1.lua @@ -1,32 +1,32 @@ local env = environment() -env = add_decl(env, mk_var_decl("A", Bool)) +env = add_decl(env, mk_var_decl("A", Prop)) local A = Const("A") env = add_decl(env, mk_axiom("H1", A)) local H1 = Const("H1") env = add_decl(env, mk_theorem("H2", A, H1)) assert(env:get("H2"):is_theorem()) -env = add_decl(env, mk_definition("B", Bool, A)) +env = add_decl(env, mk_definition("B", Prop, A)) env:export("mod1_mod.olean") local env2 = import_modules("mod1_mod.olean", {keep_proofs=true}) -assert(env2:get("A"):type() == Bool) +assert(env2:get("A"):type() == Prop) assert(env2:get("A"):is_var_decl()) assert(env2:get("H1"):type() == A) assert(env2:get("H1"):is_axiom()) assert(env2:get("H2"):type() == A) assert(env2:get("H2"):is_theorem()) assert(env2:get("H2"):value() == H1) -assert(env2:get("B"):type() == Bool) +assert(env2:get("B"):type() == Prop) assert(env2:get("B"):value() == A) assert(env2:get("B"):is_definition()) local env3 = import_modules("mod1_mod.olean") -assert(env3:get("A"):type() == Bool) +assert(env3:get("A"):type() == Prop) assert(env3:get("A"):is_var_decl()) assert(env3:get("H1"):type() == A) assert(env3:get("H1"):is_axiom()) assert(env3:get("H2"):type() == A) assert(env3:get("H2"):is_axiom()) -assert(env3:get("B"):type() == Bool) +assert(env3:get("B"):type() == Prop) assert(env3:get("B"):value() == A) assert(env3:get("B"):is_definition()) diff --git a/tests/lua/mod5.lua b/tests/lua/mod5.lua index bfe994b08..326d80936 100644 --- a/tests/lua/mod5.lua +++ b/tests/lua/mod5.lua @@ -15,13 +15,13 @@ function mk_module(midx, imports) end local env = import_modules(imp_names, {num_threads=NumThreads}) if #imports == 0 then - env = add_decl(env, mk_var_decl(const_name(midx), Bool)) - env = add_decl(env, mk_var_decl("and", mk_arrow(Bool, Bool, Bool))) + env = add_decl(env, mk_var_decl(const_name(midx), Prop)) + env = add_decl(env, mk_var_decl("and", mk_arrow(Prop, Prop, Prop))) elseif #imports == 1 then - env = add_decl(env, mk_definition(const_name(midx), Bool, Const(const_name(imports[1])))) + env = add_decl(env, mk_definition(const_name(midx), Prop, Const(const_name(imports[1])))) else local And = Const("and") - env = add_decl(env, mk_definition(const_name(midx), Bool, And(Const(const_name(imports[1])), Const(const_name(imports[2]))))) + env = add_decl(env, mk_definition(const_name(midx), Prop, And(Const(const_name(imports[1])), Const(const_name(imports[2]))))) end env:export(tostring(mod_name(midx)) .. ".olean") end diff --git a/tests/lua/place2.lua b/tests/lua/place2.lua index 80146b4d2..7bd0f3234 100644 --- a/tests/lua/place2.lua +++ b/tests/lua/place2.lua @@ -1,4 +1,4 @@ print(mk_expr_placeholder()) assert(not placeholder_type(mk_expr_placeholder())) -assert(placeholder_type(mk_expr_placeholder(Bool)) == Bool) -assert(is_placeholder(mk_expr_placeholder(Bool))) +assert(placeholder_type(mk_expr_placeholder(Prop)) == Prop) +assert(is_placeholder(mk_expr_placeholder(Prop))) diff --git a/tests/lua/proof_state1.lua b/tests/lua/proof_state1.lua index 40580d815..26a1361fc 100644 --- a/tests/lua/proof_state1.lua +++ b/tests/lua/proof_state1.lua @@ -1,6 +1,6 @@ local env = environment() local A = Local("A", Type) -env = add_decl(env, mk_var_decl("eq", Pi(A, mk_arrow(A, A, Bool)))) +env = add_decl(env, mk_var_decl("eq", Pi(A, mk_arrow(A, A, Prop)))) local eq = Const("eq") local a = mk_local("a", "a", A) local b = mk_local("b", "a", A) diff --git a/tests/lua/res1.lua b/tests/lua/res1.lua index 581d5e0ff..4aea6a4f0 100644 --- a/tests/lua/res1.lua +++ b/tests/lua/res1.lua @@ -6,14 +6,14 @@ local False = Const("false") function init_env(env) -- Populate environment when declarations used by resolve_macro. -- This is a 'fake' environment used only for testing. - local a = Local("a", Bool) - local b = Local("b", Bool) - local c = Local("c", Bool) + local a = Local("a", Prop) + local b = Local("b", Prop) + local c = Local("c", Prop) local Ha = Local("Ha", a) local Hb = Local("Hb", b) - env = add_decl(env, mk_var_decl("or", mk_arrow(Bool, Bool, Bool))) - env = add_decl(env, mk_var_decl("not", mk_arrow(Bool, Bool))) - env = add_decl(env, mk_var_decl("false", Bool)) + env = add_decl(env, mk_var_decl("or", mk_arrow(Prop, Prop, Prop))) + env = add_decl(env, mk_var_decl("not", mk_arrow(Prop, Prop))) + env = add_decl(env, mk_var_decl("false", Prop)) env = add_decl(env, mk_axiom("or_elim", Pi(a, b, c, mk_arrow(Or(a, b), mk_arrow(a, c), mk_arrow(b, c), c)))) env = add_decl(env, mk_axiom("or_intro_left", Pi(a, Ha, b, Or(a, b)))) env = add_decl(env, mk_axiom("or_intro_right", Pi(b, a, Hb, Or(a, b)))) @@ -23,7 +23,7 @@ end function decl_bools(env, ls) for i = 1, #ls do - env = add_decl(env, mk_var_decl(ls[i]:data(), Bool)) + env = add_decl(env, mk_var_decl(ls[i]:data(), Prop)) end return env end @@ -67,7 +67,7 @@ function assert_some_axioms(env) -- Assert some clauses local l1, l2, l3, l4, l5, l6 = Consts("l1 l2 l3 l4 l5 l6") env = decl_bools(env, {l1, l2, l3, l4, l5}) - env = add_decl(env, mk_definition("l6", Bool, l3, {opaque=false})) -- l6 is alias for l3 + env = add_decl(env, mk_definition("l6", Prop, l3, {opaque=false})) -- l6 is alias for l3 env = add_decl(env, mk_axiom("H1", OR(l1, l2, Not(l3)))) env = add_decl(env, mk_axiom("H2", OR(l2, l3, l4))) env = add_decl(env, mk_axiom("H3", OR(Not(l1), l2, l4, l5))) diff --git a/tests/lua/sexpr_bug1.lua b/tests/lua/sexpr_bug1.lua index 025cbee64..021effc70 100644 --- a/tests/lua/sexpr_bug1.lua +++ b/tests/lua/sexpr_bug1.lua @@ -1,20 +1,20 @@ -local s = sexpr(Local("a", Bool), Local("b", Bool)) +local s = sexpr(Local("a", Prop), Local("b", Prop)) print(s) local a, b = s:fields() print(a) print(b) -assert(a ~= Local("a", Bool)) -assert(a:to_external() == Local("a", Bool)) -assert(a:fields() == Local("a", Bool)) +assert(a ~= Local("a", Prop)) +assert(a:to_external() == Local("a", Prop)) +assert(a:fields() == Local("a", Prop)) assert(is_expr(a:to_external())) -local s = sexpr(Local("a", Bool), Local("b", Bool)) +local s = sexpr(Local("a", Prop), Local("b", Prop)) local s = sexpr({}) -local s1 = sexpr(Local("a", Bool), Local("b", Bool)) -local s2 = sexpr(Local("a", Bool), Local("c", Bool)) -assert(Local("b", Bool) > Local("c", Bool)) +local s1 = sexpr(Local("a", Prop), Local("b", Prop)) +local s2 = sexpr(Local("a", Prop), Local("c", Prop)) +assert(Local("b", Prop) > Local("c", Prop)) assert(s1 > s2) assert(s2 < s1) -assert(s2 == sexpr(Local("a", Bool), Local("c", Bool))) +assert(s2 == sexpr(Local("a", Prop), Local("c", Prop))) diff --git a/tests/lua/slow/mod2.lua b/tests/lua/slow/mod2.lua index 99b4dbdab..a2beebaa0 100644 --- a/tests/lua/slow/mod2.lua +++ b/tests/lua/slow/mod2.lua @@ -4,7 +4,7 @@ function mk_env(prefix, sz) local A = Local("A", mk_sort(0)) local x = Local("x", A) env = add_decl(env, mk_definition(name(prefix, "id"), Pi(A, mk_arrow(A, A)), Fun(A, x, x), {opaque=false})) - env = add_decl(env, mk_var_decl(name(prefix, "P"), Bool)) + env = add_decl(env, mk_var_decl(name(prefix, "P"), Prop)) local P = Const(name(prefix, "P")) local id = Const(name(prefix, "id")) env = add_decl(env, mk_axiom(name(prefix, "Ax"), P)) diff --git a/tests/lua/sorted.lua b/tests/lua/sorted.lua index e00bba557..a565dc70d 100644 --- a/tests/lua/sorted.lua +++ b/tests/lua/sorted.lua @@ -2,7 +2,7 @@ local env = environment() local l = mk_param_univ("l") local A = Local("A", mk_sort(l)) local U_l = mk_sort(l) -local U_l1 = mk_sort(max_univ(l, 1)) -- Make sure U_l1 is not Bool/Prop +local U_l1 = mk_sort(max_univ(l, 1)) -- Make sure U_l1 is not Prop local list_l = Const("list", {l}) -- list.{l} env = add_inductive(env, @@ -14,7 +14,7 @@ local cons_l = Const("cons", {l}) local nil_l = Const("nil", {l}) local is_sorted_l = Const("is_sorted", {l}) local a = Local("a", A) -local lt = Local("lt", mk_arrow(A, A, Bool)) +local lt = Local("lt", mk_arrow(A, A, Prop)) local a1 = Local("a1", A) local a2 = Local("a2", A) local t = Local("t", list_l(A)) @@ -22,7 +22,7 @@ local Hlt = Local("H", lt(a1, a2)) local Hs = Local("Hs", is_sorted_l(A, lt, cons_l(A, a2, t))) env = add_inductive(env, - "is_sorted", {l}, 2, Pi(A, lt, mk_arrow(list_l(A), Bool)), + "is_sorted", {l}, 2, Pi(A, lt, mk_arrow(list_l(A), Prop)), "is_sorted_nil", Pi(A, lt, is_sorted_l(A, lt, nil_l(A))), "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))))) diff --git a/tests/lua/subst1.lua b/tests/lua/subst1.lua index c7383a264..1826c6a26 100644 --- a/tests/lua/subst1.lua +++ b/tests/lua/subst1.lua @@ -1,4 +1,4 @@ -local m = mk_metavar("m", Bool) +local m = mk_metavar("m", Prop) local s = substitution() assert(not s:is_assigned(m)) assert(not s:is_expr_assigned("m")) @@ -21,7 +21,7 @@ assert(s:is_assigned(u)) assert(s:is_level_assigned("u")) assert(not s:is_expr_assigned("u")) assert(s:get_expr("m") == a) -local m2 = mk_metavar("m2", Bool) +local m2 = mk_metavar("m2", Prop) s = s:assign(m2, f(m)) print(s:get_expr("m2")) assert(s:occurs(m, f(m2))) diff --git a/tests/lua/tactic1.lua b/tests/lua/tactic1.lua index 260ebd755..acb5acf3a 100644 --- a/tests/lua/tactic1.lua +++ b/tests/lua/tactic1.lua @@ -1,6 +1,6 @@ local env = environment() local A = Local("A", Type) -env = add_decl(env, mk_var_decl("eq", Pi(A, mk_arrow(A, A, Bool)))) +env = add_decl(env, mk_var_decl("eq", Pi(A, mk_arrow(A, A, Prop)))) local eq = Const("eq") local a = Local("a", A) local b = Local("b", A) diff --git a/tests/lua/tag1.lua b/tests/lua/tag1.lua index cf1461041..fc025d70f 100644 --- a/tests/lua/tag1.lua +++ b/tests/lua/tag1.lua @@ -1,5 +1,5 @@ local f = Const("f") -local x = Local("x", Bool) +local x = Local("x", Prop) local a = Const("a") local t1 = f(x, a, Var(1)) local t2 = Fun(x, t1) diff --git a/tests/lua/tc1.lua b/tests/lua/tc1.lua index c9b14ffef..f57a28495 100644 --- a/tests/lua/tc1.lua +++ b/tests/lua/tc1.lua @@ -2,12 +2,12 @@ local env = bare_environment() local g = name_generator("tst") local tc = type_checker(env, g) assert(is_type_checker(tc)) -local a = Local("a", Bool) +local a = Local("a", Prop) local t = Fun(a, a) local b = Const("b") print(t(b)) assert(tc:whnf(t(b)) == b) -assert(tc:check(Bool) == mk_sort(mk_level_one())) +assert(tc:check(Prop) == mk_sort(mk_level_one())) print(tc:infer(t)) local m = mk_metavar("m1", mk_metavar("m2", mk_sort(mk_meta_univ("u")))) print(tc:infer(m)) diff --git a/tests/lua/tc2.lua b/tests/lua/tc2.lua index a0339bdac..46333764c 100644 --- a/tests/lua/tc2.lua +++ b/tests/lua/tc2.lua @@ -3,9 +3,9 @@ local l = mk_param_univ("l") local A = Local("A", mk_sort(l)) local a = Local("a", A) local b = Local("b", A) -local P = Local("P", mk_arrow(A, Bool)) +local P = Local("P", mk_arrow(A, Prop)) env = add_decl(env, mk_definition("id", {l}, - Pi(A, mk_arrow(A, mk_arrow(A, Bool))), + Pi(A, mk_arrow(A, mk_arrow(A, Prop))), Fun(A, a, b, Pi(P, mk_arrow(P(a), P(b)))))) local id_l = Const("id", {l}) local H = Local("H", P(a)) diff --git a/tests/lua/tc4.lua b/tests/lua/tc4.lua index b6ec5f154..d67138066 100644 --- a/tests/lua/tc4.lua +++ b/tests/lua/tc4.lua @@ -1,12 +1,12 @@ local env = bare_environment() -env = add_decl(env, mk_var_decl("or", mk_arrow(Bool, Bool, Bool))) -env = add_decl(env, mk_var_decl("A", Bool)) +env = add_decl(env, mk_var_decl("or", mk_arrow(Prop, Prop, Prop))) +env = add_decl(env, mk_var_decl("A", Prop)) local Or = Const("or") local A = Const("A") local B = Const("B") local tc = type_checker(env) local F = Or(A, B) -assert(tc:infer(F) == Bool) +assert(tc:infer(F) == Prop) assert(not pcall(function() -- The following test must fail since B is not -- declared in env. diff --git a/tests/lua/tc5.lua b/tests/lua/tc5.lua index 7a495ed17..9fd02ba2e 100644 --- a/tests/lua/tc5.lua +++ b/tests/lua/tc5.lua @@ -1,9 +1,9 @@ local env = bare_environment() -env = add_decl(env, mk_var_decl("A", Bool)) +env = add_decl(env, mk_var_decl("A", Prop)) env = add_decl(env, mk_var_decl("T", Type)) -env = add_decl(env, mk_definition("B2", Type, Bool, {opaque=false})) +env = add_decl(env, mk_definition("B2", Type, Prop, {opaque=false})) env = add_decl(env, mk_var_decl("C", Const("B2"))) -env = add_decl(env, mk_definition("BB", Type, mk_arrow(Bool, Bool), {opaque=false})) +env = add_decl(env, mk_definition("BB", Type, mk_arrow(Prop, Prop), {opaque=false})) local tc = type_checker(env) assert(tc:is_prop(Const("A"))) assert(tc:is_prop(Const("C"))) @@ -22,7 +22,7 @@ assert(not pcall(function() end )) assert(not pcall(function() - env = add_decl(env, mk_var_decl("A", mk_local("l1", Bool))) + env = add_decl(env, mk_var_decl("A", mk_local("l1", Prop))) end )) assert(not pcall(function() @@ -30,7 +30,7 @@ assert(not pcall(function() end )) assert(not pcall(function() - print(tc:check(mk_lambda("x", Bool, Var(0))(Type))) + print(tc:check(mk_lambda("x", Prop, Var(0))(Type))) end )) assert(not pcall(function() @@ -38,8 +38,8 @@ assert(not pcall(function() end )) -assert(tc:check(mk_pi("x", Bool, Var(0))) == Bool) +assert(tc:check(mk_pi("x", Prop, Var(0))) == Prop) local env = bare_environment({impredicative=false}) local tc = type_checker(env) -assert(tc:check(mk_pi("x", Bool, Var(0))) == Type) +assert(tc:check(mk_pi("x", Prop, Var(0))) == Type) diff --git a/tests/lua/tc_bug1.lua b/tests/lua/tc_bug1.lua index 233981b10..ef7b06e73 100644 --- a/tests/lua/tc_bug1.lua +++ b/tests/lua/tc_bug1.lua @@ -9,16 +9,16 @@ local H1 = Const("H1") local H2 = Const("H2") local And = Const("and") local and_intro = Const("and_intro") -local A = Local("A", Bool) -local B = Local("B", Bool) -local C = Local("C", Bool) +local A = Local("A", Prop) +local B = Local("B", Prop) +local C = Local("C", Prop) env = add_decl(env, mk_var_decl("N", Type)) -env = add_decl(env, mk_var_decl("p", mk_arrow(N, N, Bool))) -env = add_decl(env, mk_var_decl("q", mk_arrow(N, Bool))) +env = add_decl(env, mk_var_decl("p", mk_arrow(N, N, Prop))) +env = add_decl(env, mk_var_decl("q", mk_arrow(N, Prop))) env = add_decl(env, mk_var_decl("f", mk_arrow(N, N))) env = add_decl(env, mk_var_decl("a", N)) env = add_decl(env, mk_var_decl("b", N)) -env = add_decl(env, mk_var_decl("and", mk_arrow(Bool, Bool, Bool))) +env = add_decl(env, mk_var_decl("and", mk_arrow(Prop, Prop, Prop))) env = add_decl(env, mk_var_decl("and_intro", Pi(A, B, mk_arrow(A, B, And(A, B))))) env = add_decl(env, mk_var_decl("foo_intro", Pi(A, B, C, mk_arrow(B, B)))) env = add_decl(env, mk_var_decl("foo_intro2", Pi(A, B, C, mk_arrow(B, B)))) @@ -32,7 +32,7 @@ local foo_intro = Const("foo_intro") local foo_intro2 = Const("foo_intro2") local ng = name_generator("foo") local tc = type_checker(env, ng) -local m1 = mk_metavar("m1", Bool) +local m1 = mk_metavar("m1", Prop) print("before is_def_eq") assert(not tc:next_cnstr()) local tc = type_checker(env, ng) diff --git a/tests/lua/unify1.lua b/tests/lua/unify1.lua index bb6948170..cad9e61fd 100644 --- a/tests/lua/unify1.lua +++ b/tests/lua/unify1.lua @@ -15,10 +15,10 @@ end local f = Const("f") local a = Const("a") -local l1 = mk_local("l1", "x", Bool) -local l2 = mk_local("l2", "y", Bool) -local l3 = mk_local("l3", "z", Bool) -local m = mk_metavar("m", Bool) +local l1 = mk_local("l1", "x", Prop) +local l2 = mk_local("l2", "y", Prop) +local l3 = mk_local("l3", "z", Prop) +local m = mk_metavar("m", Prop) test_unify_simple(m(l1, l2), f(f(a, l1), l1), unify_status.Solved) test_unify_simple(m(l1, l2), m(l1, l2), unify_status.Solved) diff --git a/tests/lua/unify4.lua b/tests/lua/unify4.lua index 8b6f6032a..a94af1e47 100644 --- a/tests/lua/unify4.lua +++ b/tests/lua/unify4.lua @@ -23,4 +23,4 @@ local l3 = mk_local("l3", "z", N) local m = mk_metavar("m", mk_arrow(N, N, mk_metavar("m_type", mk_arrow(N, N, mk_sort(mk_meta_univ("u"))))(Var(1), Var(0)))) test_unify(env, m, m(l1, l1), f(f(a, l1), l1), 4) print("-----------------") -test_unify(env, m, m(l1, l1), mk_lambda("z", Bool, f(l1, f(Var(0), a))), 2) +test_unify(env, m, m(l1, l1), mk_lambda("z", Prop, f(l1, f(Var(0), a))), 2) diff --git a/tests/lua/unify7.lua b/tests/lua/unify7.lua index 2bb5e428b..8563d1ae7 100644 --- a/tests/lua/unify7.lua +++ b/tests/lua/unify7.lua @@ -2,10 +2,10 @@ local env = environment() local N = Const("N") local P = Const("P") env = add_decl(env, mk_var_decl("N", Type)) -env = add_decl(env, mk_var_decl("P", mk_arrow(N, Bool))) +env = add_decl(env, mk_var_decl("P", mk_arrow(N, Prop))) local a = Local("a", N) local H = Local("H", P(a)) -local t = Pi(H, Bool) +local t = Pi(H, Prop) print(env:infer_type(t)) local m = mk_metavar("m", mk_arrow(N, N, Type)) local cs = { mk_eq_cnstr(m(a, a), t) }