lean2/tests/lean/run/class4.lean

92 lines
2.3 KiB
Text
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

import logic
inductive nat : Type :=
zero : nat,
succ : nat → nat
open eq
namespace nat
definition add (x y : nat)
:= nat.rec x (λ n r, succ r) y
infixl `+` := add
theorem add_zero_left (x : nat) : x + zero = x
:= refl _
theorem add_succ_left (x y : nat) : x + (succ y) = succ (x + y)
:= refl _
definition is_zero (x : nat)
:= nat.rec true (λ n r, false) x
theorem is_zero_zero : is_zero zero
:= eq_true_elim (refl _)
theorem not_is_zero_succ (x : nat) : ¬ is_zero (succ x)
:= eq_false_elim (refl _)
theorem dichotomy (m : nat) : m = zero (∃ n, m = succ n)
:= nat.rec
(or.intro_left _ (refl zero))
(λ m H, or.intro_right _ (exists_intro m (refl (succ m))))
m
theorem is_zero_to_eq (x : nat) (H : is_zero x) : x = zero
:= or.elim (dichotomy x)
(assume Hz : x = zero, Hz)
(assume Hs : (∃ n, x = succ n),
exists_elim Hs (λ (w : nat) (Hw : x = succ w),
absurd H (eq.subst (symm Hw) (not_is_zero_succ w))))
theorem is_not_zero_to_eq {x : nat} (H : ¬ is_zero x) : ∃ n, x = succ n
:= or.elim (dichotomy x)
(assume Hz : x = zero,
absurd (eq.subst (symm Hz) is_zero_zero) H)
(assume Hs, Hs)
theorem not_zero_add (x y : nat) (H : ¬ is_zero y) : ¬ is_zero (x + y)
:= exists_elim (is_not_zero_to_eq H)
(λ (w : nat) (Hw : y = succ w),
have H1 : x + y = succ (x + w), from
calc x + y = x + succ w : {Hw}
... = succ (x + w) : refl _,
have H2 : ¬ is_zero (succ (x + w)), from
not_is_zero_succ (x+w),
subst (symm H1) H2)
inductive not_zero [class] (x : nat) : Prop :=
intro : ¬ is_zero x → not_zero x
theorem not_zero_not_is_zero {x : nat} (H : not_zero x) : ¬ is_zero x
:= not_zero.rec (λ H1, H1) H
theorem not_zero_add_right [instance] (x y : nat) (H : not_zero y) : not_zero (x + y)
:= not_zero.intro (not_zero_add x y (not_zero_not_is_zero H))
theorem not_zero_succ [instance] (x : nat) : not_zero (succ x)
:= not_zero.intro (not_is_zero_succ x)
constant dvd : Π (x y : nat) {H : not_zero y}, nat
constants a b : nat
set_option pp.implicit true
reducible add
check dvd a (succ b)
check (λ H : not_zero b, dvd a b)
check (succ zero)
check a + (succ zero)
check dvd a (a + (succ b))
reducible [off] add
check dvd a (a + (succ b))
reducible add
check dvd a (a + (succ b))
reducible [off] add
check dvd a (a + (succ b))
end nat