From d43bf5cc314729905d4b65d51f0c1a6438e091a5 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 14 Sep 2005 08:04:32 +0000 Subject: [PATCH] Product, pair and projections. --- helm/matita/library/datatypes/constructors.ma | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/helm/matita/library/datatypes/constructors.ma b/helm/matita/library/datatypes/constructors.ma index c2bdc566b..2ac1cb376 100644 --- a/helm/matita/library/datatypes/constructors.ma +++ b/helm/matita/library/datatypes/constructors.ma @@ -13,12 +13,26 @@ (**************************************************************************) set "baseuri" "cic:/matita/datatypes/constructors/". +include "logic/equality.ma". inductive void : Set \def. inductive Prod (A,B:Set) : Set \def pair : A \to B \to Prod A B. +definition fst \def \lambda A,B:Set.\lambda p: Prod A B. +match p with +[(pair a b) \Rightarrow a]. + +definition snd \def \lambda A,B:Set.\lambda p: Prod A B. +match p with +[(pair a b) \Rightarrow b]. + +theorem eq_pair_fst_snd: \forall A,B:Set.\forall p: Prod A B. +p = pair A B (fst A B p) (snd A B p). +intros.elim p.simplify.reflexivity. +qed. + inductive Sum (A,B:Set) : Set \def inl : A \to Sum A B -| inr : B \to Sum A B. \ No newline at end of file +| inr : B \to Sum A B. -- 2.39.2