ninductive True: Prop ≝
I : True.
-ndefinition True_ind : ΠP:Prop.P → True → P ≝
-λP:Prop.λp:P.λH:True.
- match H with [ I ⇒ p ].
-
-ndefinition True_rec : ΠP:Set.P → True → P ≝
-λP:Set.λp:P.λH:True.
- match H with [ I ⇒ p ].
-
-ndefinition True_rect : ΠP:Type.P → True → P ≝
-λP:Type.λp:P.λH:True.
- match H with [ I ⇒ p ].
-
ninductive False: Prop ≝.
-ndefinition False_ind : ΠP:Prop.False → P ≝
-λP:Prop.λH:False.
- match H in False return λH1:False.P with [].
-
-ndefinition False_rec : ΠP:Set.False → P ≝
-λP:Set.λH:False.
- match H in False return λH1:False.P with [].
-
-ndefinition False_rect : ΠP:Type.False → P ≝
-λP:Type.λH:False.
- match H in False return λH1:False.P with [].
-
ndefinition Not: Prop → Prop ≝
λA.(A → False).
#A; #C; #H;
nnormalize;
#H1;
- nelim (H1 H).
+ nelim (H1 H);
nqed.
nlemma not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A.
ninductive And (A,B:Prop) : Prop ≝
conj : A → B → (And A B).
-ndefinition And_ind : ΠA,B:Prop.ΠP:Prop.(A → B → P) → And A B → P ≝
-λA,B:Prop.λP:Prop.λf:A → B → P.λH:And A B.
- match H with [conj H1 H2 ⇒ f H1 H2 ].
-
-ndefinition And_rec : ΠA,B:Prop.ΠP:Set.(A → B → P) → And A B → P ≝
-λA,B:Prop.λP:Set.λf:A → B → P.λH:And A B.
- match H with [conj H1 H2 ⇒ f H1 H2 ].
-
-ndefinition And_rect : ΠA,B:Prop.ΠP:Type.(A → B → P) → And A B → P ≝
-λA,B:Prop.λP:Type.λf:A → B → P.λH:And A B.
- match H with [conj H1 H2 ⇒ f H1 H2 ].
-
interpretation "logical and" 'and x y = (And x y).
nlemma proj1: ∀A,B:Prop.A ∧ B → A.
#A; #B; #H;
- napply (And_ind A B ?? H);
+ napply (And_ind A B … H);
#H1; #H2;
napply H1.
nqed.
nlemma proj2: ∀A,B:Prop.A ∧ B → B.
#A; #B; #H;
- napply (And_ind A B ?? H);
+ napply (And_ind A B … H);
#H1; #H2;
napply H2.
nqed.
or_introl : A → (Or A B)
| or_intror : B → (Or A B).
-ndefinition Or_ind : ΠA,B:Prop.ΠP:Prop.(A → P) → (B → P) → Or A B → P ≝
-λA,B:Prop.λP:Prop.λf1:A → P.λf2:B → P.λH:Or A B.
- match H with [ or_introl H1 ⇒ f1 H1 | or_intror H1 ⇒ f2 H1 ].
-
interpretation "logical or" 'or x y = (Or x y).
ndefinition decidable : Prop → Prop ≝ λA:Prop.A ∨ ¬A.
ninductive ex (A:Type) (Q:A → Prop) : Prop ≝
ex_intro: ∀x:A.Q x → ex A Q.
-ndefinition ex_ind : ΠA:Type.ΠQ:A → Prop.ΠP:Prop.(Πa:A.Q a → P) → ex A Q → P ≝
-λA:Type.λQ:A → Prop.λP:Prop.λf:(Πa:A.Q a → P).λH:ex A Q.
- match H with [ ex_intro H1 H2 ⇒ f H1 H2 ].
-
interpretation "exists" 'exists x = (ex ? x).
ninductive ex2 (A:Type) (Q,R:A → Prop) : Prop ≝
ex_intro2: ∀x:A.Q x → R x → ex2 A Q R.
-ndefinition ex2_ind : ΠA:Type.ΠQ,R:A → Prop.ΠP:Prop.(Πa:A.Q a → R a → P) → ex2 A Q R → P ≝
-λA:Type.λQ,R:A → Prop.λP:Prop.λf:(Πa:A.Q a → R a → P).λH:ex2 A Q R.
- match H with [ ex_intro2 H1 H2 H3 ⇒ f H1 H2 H3 ].
-
ndefinition iff ≝
λA,B.(A -> B) ∧ (B -> A).
ninductive eq (A:Type) (x:A) : A → Prop ≝
refl_eq : eq A x x.
-ndefinition eq_ind : ΠA:Type.Πx:A.ΠP:A → Prop.P x → Πa:A.eq A x a → P a ≝
-λA:Type.λx:A.λP:A → Prop.λp:P x.λa:A.λH:eq A x a.
- match H with [refl_eq ⇒ p ].
-
-ndefinition eq_rec : ΠA:Type.Πx:A.ΠP:A → Set.P x → Πa:A.eq A x a → P a ≝
-λA:Type.λx:A.λP:A → Set.λp:P x.λa:A.λH:eq A x a.
- match H with [refl_eq ⇒ p ].
-
-ndefinition eq_rect : ΠA:Type.Πx:A.ΠP:A → Type.P x → Πa:A.eq A x a → P a ≝
-λA:Type.λx:A.λP:A → Type.λp:P x.λa:A.λH:eq A x a.
- match H with [refl_eq ⇒ p ].
-
interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
nnormalize;
#x; #y; #H;
nrewrite < H;
- napply (refl_eq ??).
+ napply refl_eq.
nqed.
nlemma eq_elim_r: ∀A:Type.∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
#A; #x; #P; #H; #y; #H1;
- napply (eq_ind ? x ? H y ?);
- nrewrite < H1;
- napply (refl_eq ??).
+ nrewrite < (symmetric_eq … H1);
+ napply H.
nqed.
ndefinition relationT : Type → Type → Type ≝
nil: list A
| cons: A -> list A -> list A.
-nlet rec list_ind (A:Type) (P:list A → Prop) (p:P (nil A)) (f:(Πa:A.Πl':list A.P l' → P (cons A a l'))) (l:list A) on l ≝
- match l with [ nil ⇒ p | cons h t ⇒ f h t (list_ind A P p f t) ].
-
-nlet rec list_rec (A:Type) (P:list A → Set) (p:P (nil A)) (f:Πa:A.Πl':list A.P l' → P (cons A a l')) (l:list A) on l ≝
- match l with [ nil ⇒ p | cons h t ⇒ f h t (list_rec A P p f t) ].
-
-nlet rec list_rect (A:Type) (P:list A → Type) (p:P (nil A)) (f:Πa:A.Πl':list A.P l' → P (cons A a l')) (l:list A) on l ≝
- match l with [ nil ⇒ p | cons h t ⇒ f h t (list_rect A P p f t) ].
-
nlet rec append A (l1: list A) l2 on l1 ≝
match l1 with
[ nil => l2
nchange with (match cons T x2 y2 with [ nil ⇒ False | cons a _ ⇒ x1 = a ]);
nrewrite < H;
nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
nqed.
nlemma list_destruct_2 : ∀T.∀x1,x2:T.∀y1,y2:list T.cons T x1 y1 = cons T x2 y2 → y1 = y2.
nchange with (match cons T x2 y2 with [ nil ⇒ False | cons _ b ⇒ y1 = b ]);
nrewrite < H;
nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
nqed.
nlemma list_destruct_cons_nil : ∀T.∀x:T.∀y:list T.cons T x y = nil T → False.
nlemma append_nil : ∀T:Type.∀l:list T.(l@[]) = l.
#T; #l;
- napply (list_ind T ??? l);
+ nelim l;
nnormalize;
- ##[ ##1: napply (refl_eq ??)
+ ##[ ##1: napply refl_eq
##| ##2: #x; #y; #H;
nrewrite > H;
- napply (refl_eq ??)
+ napply refl_eq
##]
nqed.
nlemma associative_list : ∀T.associative (list T) (append T).
#T; #x; #y; #z;
- napply (list_ind T ??? x);
+ nelim x;
nnormalize;
- ##[ ##1: napply (refl_eq ??)
+ ##[ ##1: napply refl_eq
##| ##2: #a; #b; #H;
nrewrite > H;
- napply (refl_eq ??)
+ napply refl_eq
##]
nqed.
nlemma cons_append_commute : ∀T:Type.∀l1,l2:list T.∀a:T.a :: (l1 @ l2) = (a :: l1) @ l2.
#T; #l1; #l2; #a;
nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
nqed.
nlemma append_cons_commute : ∀T:Type.∀a:T.∀l,l1:list T.l @ (a::l1) = (l@[a]) @ l1.
#T; #a; #l; #l1;
nrewrite > (associative_list T l [a] l1);
nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
nqed.
projects / helm.git / blobdiff