From 6003ba0e4600778c6055ed5ea5cb6c1fba3abe32 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 13 Jul 2009 09:13:12 +0000 Subject: [PATCH 1/1] First proof finished (some tactics still not working). --- helm/software/matita/nlibrary/algebra/magmas.ma | 9 ++++++++- helm/software/matita/nlibrary/logic/equality.ma | 5 +++++ 2 files changed, 13 insertions(+), 1 deletion(-) diff --git a/helm/software/matita/nlibrary/algebra/magmas.ma b/helm/software/matita/nlibrary/algebra/magmas.ma index 7283cbc58..4fac05b51 100644 --- a/helm/software/matita/nlibrary/algebra/magmas.ma +++ b/helm/software/matita/nlibrary/algebra/magmas.ma @@ -47,6 +47,10 @@ ndefinition mmcarr ≝ λA,B.λf: pre_magma_morphism A B. match f with [ mk_pre_magma_morphism f _ ⇒ f ]. ncoercion mmcarr: ∀A,B.∀M: pre_magma_morphism A B. A → B ≝ mmcarr on _M: pre_magma_morphism ? ? to ∀_.?. +ndefinition mmprop ≝ + λA,B,M. + match M return λM:pre_magma_morphism A B.∀x,y. M (op ? x y) = op ? (M x) (M y) with + [ mk_pre_magma_morphism _ p ⇒ p ]. nrecord magma_morphism (A) (B) (Ma: magma A) (Mb: magma B) : Type ≝ { mmmcarr: pre_magma_morphism A B; @@ -81,5 +85,8 @@ ndefinition mm_image: [ napply (op ? x0 y0) | napply (conj ????) [ napply (op_closed ??????); nassumption - | nelim daemon ]##] + | (* nrewrite < Hx1; DOES NOT WORK *) + napply (eq_rect ?? (λ_.?) ?? Hx1); + napply (eq_rect ?? (λ_.?) ?? Hy1); + napply (mmprop ?? f ??)]##] nqed. \ No newline at end of file diff --git a/helm/software/matita/nlibrary/logic/equality.ma b/helm/software/matita/nlibrary/logic/equality.ma index ff8cc5a13..2418f2a7c 100644 --- a/helm/software/matita/nlibrary/logic/equality.ma +++ b/helm/software/matita/nlibrary/logic/equality.ma @@ -16,6 +16,11 @@ include "logic/connectives.ma". ninductive eq (A: Type) (a: A) : A → CProp ≝ refl: eq A a a. + +nlet rec eq_rect (A: Type) (x: A) (P: ∀y:A. eq A x y → CProp) (q: P x (refl A x)) + (y: A) (p: eq A x y) on p : P y p ≝ + match p with + [ refl ⇒ q ]. interpretation "leibnitz's equality" 'eq t x y = (eq t x y). -- 2.39.2