From 69e7d276ed3d68ae78d5e8091cc19c714c69572c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 21 Nov 2005 18:07:27 +0000 Subject: [PATCH] Useful lemma added. --- helm/matita/library/datatypes/bool.ma | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/helm/matita/library/datatypes/bool.ma b/helm/matita/library/datatypes/bool.ma index f4aec8167..3292e6789 100644 --- a/helm/matita/library/datatypes/bool.ma +++ b/helm/matita/library/datatypes/bool.ma @@ -62,15 +62,21 @@ definition andb : bool \to bool \to bool\def [ true \Rightarrow b2 | false \Rightarrow false ]. +(*CSC: the URI must disappear: there is a bug now *) +interpretation "boolean and" 'and x y = (cic:/matita/datatypes/bool/andb.con x y). + theorem andb_elim: \forall b1,b2:bool. \forall P:bool \to Prop. match b1 with [ true \Rightarrow P b2 -| false \Rightarrow P false] \to P (andb b1 b2). +| false \Rightarrow P false] \to P (b1 \land b2). intros 3.elim b1.exact H. exact H. qed. -(*CSC: the URI must disappear: there is a bug now *) -interpretation "boolean and" 'and x y = (cic:/matita/datatypes/bool/andb.con x y). +theorem andb_true_true: \forall b1,b2. (b1 \land b2) = true \to b1 = true. +intro. elim b1. +reflexivity. +assumption. +qed. definition orb : bool \to bool \to bool\def \lambda b1,b2:bool. -- 2.39.2