From adc7a41ccbed2f36778c662d8a2ce06e192fb555 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 23 Mar 2010 15:51:56 +0000 Subject: [PATCH] Commented a few lemmas (copies). From: asperti --- helm/software/matita/nlibrary/basics/eq.ma | 11 +++++++---- helm/software/matita/nlibrary/basics/list.ma | 3 ++- 2 files changed, 9 insertions(+), 5 deletions(-) diff --git a/helm/software/matita/nlibrary/basics/eq.ma b/helm/software/matita/nlibrary/basics/eq.ma index 61047a474..56a733378 100644 --- a/helm/software/matita/nlibrary/basics/eq.ma +++ b/helm/software/matita/nlibrary/basics/eq.ma @@ -16,11 +16,13 @@ include "basics/relations.ma". interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)). +(* this is refl ntheorem reflexive_eq : ∀A:Type. reflexive A (eq A). -//; nqed. - +//; nqed. *) + +(* this is sym_eq ntheorem symmetric_eq: ∀A:Type. symmetric A (eq A). -//; nqed. +//; nqed. *) ntheorem transitive_eq : ∀A:Type. transitive A (eq A). #A; #x; #y; #z; #H1; #H2; nrewrite > H1; //; nqed. @@ -46,7 +48,8 @@ theorem eq_f': \forall A,B:Type.\forall f:A\to B. intros.elim H.apply refl_eq. qed. *) +(* deleterio per auto ntheorem eq_f2: ∀A,B,C:Type.∀f:A→B→C. ∀x1,x2:A.∀y1,y2:B. x1=x2 → y1=y2 → f x1 y1 = f x2 y2. #A; #B; #C; #f; #x1; #x2; #y1; #y2; #E1; #E2; nrewrite > E1; nrewrite > E2;//. -nqed. \ No newline at end of file +nqed. *) \ No newline at end of file diff --git a/helm/software/matita/nlibrary/basics/list.ma b/helm/software/matita/nlibrary/basics/list.ma index d30ed7dfc..3d41b946c 100644 --- a/helm/software/matita/nlibrary/basics/list.ma +++ b/helm/software/matita/nlibrary/basics/list.ma @@ -73,10 +73,11 @@ ntheorem associative_append: ∀A:Type.associative (list A) (append A). #A; #l1; #l2; #l3; nelim l1; nnormalize; //; nqed. +(* deleterio per auto ntheorem cons_append_commute: ∀A:Type.∀l1,l2:list A.∀a:A. a :: (l1 @ l2) = (a :: l1) @ l2. -//; nqed. +//; nqed. *) ntheorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1. #A; #a; #l; #l1; napply symmetric_eq. -- 2.39.2