From 6a149d262dfcb03a7d57f8ecabf23b0b59e99f85 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 12 Dec 2005 16:02:05 +0000 Subject: [PATCH] coercion command now requires an uri --- .../PREDICATIVE-TOPOLOGY/class_defs.ma | 4 +- .../PREDICATIVE-TOPOLOGY/domain_defs.ma | 4 +- .../PREDICATIVE-TOPOLOGY/subset_defs.ma | 2 +- helm/matita/library/Z/z.ma | 2 +- helm/matita/library/list/list.ma | 44 ++++++++++--------- helm/matita/tests/coercions.ma | 6 +-- 6 files changed, 31 insertions(+), 31 deletions(-) diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma index ba1195619..acd73c4ba 100644 --- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma +++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma @@ -37,13 +37,11 @@ definition true_f \def \lambda (X:Type). \lambda (_:X). True. definition false_f \def \lambda (X:Type). \lambda (_:X). False. record Class: Type \def { - class: Type; + class:> Type; cin : class \to Prop; cle1 : class \to class \to Prop }. -coercion class. - inductive ceq (C:Class) (c1:C): C \to Prop \def | ceq_refl: cin ? c1 \to ceq ? c1 c1 | ceq_sing_r: \forall c2,c3. diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma index 916c91cd8..68cbd01fa 100644 --- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma +++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma @@ -24,11 +24,9 @@ include "class_defs.ma". *) record Domain: Type \def { - qd: Class + qd:> Class }. -coercion qd. - (* internal universal quantification *) inductive dall (D:Domain) (P:D \to Prop) : Prop \def | dall_intro: (\forall d:D. cin D d \to P d) \to dall D P. diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma index 3cc583f02..cf981362c 100644 --- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma +++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma @@ -60,7 +60,7 @@ definition domain_of_subset: \forall D. (Subset D) \to Domain \def \lambda (D:Domain). \lambda U. mk_Domain (mk_Class D (sin D U) (cle1 D)). -coercion domain_of_subset. +coercion cic:/matita/PREDICATIVE-TOPOLOGY/subset_defs/domain_of_subset.con. (* the full subset of a domain *) coercion stop. diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma index d18c80b23..ea50a2cd9 100644 --- a/helm/matita/library/Z/z.ma +++ b/helm/matita/library/Z/z.ma @@ -27,7 +27,7 @@ definition Z_of_nat \def [ O \Rightarrow OZ | (S n)\Rightarrow pos n]. -coercion Z_of_nat. +coercion cic:/matita/Z/z/Z_of_nat.con. definition neg_Z_of_nat \def \lambda n. match n with diff --git a/helm/matita/library/list/list.ma b/helm/matita/library/list/list.ma index d5664f416..ffa2c8ef9 100644 --- a/helm/matita/library/list/list.ma +++ b/helm/matita/library/list/list.ma @@ -16,6 +16,10 @@ set "baseuri" "cic:/matita/list/". include "logic/equality.ma". include "higher_order_defs/functions.ma". +inductive list (A:Set) : Set := + | nil: list A + | cons: A -> list A -> list A. + notation "hvbox(hd break :: tl)" right associative with precedence 46 for @{'cons $hd $tl}. @@ -28,10 +32,6 @@ notation "hvbox(l1 break @ l2)" right associative with precedence 47 for @{'append $l1 $l2 }. -inductive list (A:Set) : Set := - | nil: list A - | cons: A -> list A -> list A. - interpretation "nil" 'nil = (cic:/matita/list/list.ind#xpointer(1/1/1) _). interpretation "cons" 'cons hd tl = (cic:/matita/list/list.ind#xpointer(1/1/2) _ hd tl). @@ -41,8 +41,9 @@ interpretation "cons" 'cons hd tl = theorem nil_cons: \forall A:Set.\forall l:list A.\forall a:A. a::l <> []. - intros. - unfold; intros. + intros; + unfold Not; + intros; discriminate H. qed. @@ -64,28 +65,31 @@ definition tail := \lambda A:Set. \lambda l: list A. interpretation "append" 'append l1 l2 = (cic:/matita/list/append.con _ l1 l2). theorem append_nil: \forall A:Set.\forall l:list A.l @ [] = l. - intros. - elim l. - reflexivity. - simplify. - rewrite > H. - reflexivity. + intros; + elim l; + [ reflexivity; + | simplify; + rewrite > H; + reflexivity; + ] qed. theorem associative_append: \forall A:Set.associative (list A) (append A). - intros; unfold; intros. - elim x. - simplify; reflexivity. - simplify. - rewrite > H. - reflexivity. + intros; unfold; intros; + elim x; + [ simplify; + reflexivity; + | simplify; + rewrite > H; + reflexivity; + ] qed. theorem cons_append_commute: \forall A:Set.\forall l1,l2:list A.\forall a:A. a :: (l1 @ l2) = (a :: l1) @ l2. - intros. - reflexivity. + intros; + reflexivity; qed. (* diff --git a/helm/matita/tests/coercions.ma b/helm/matita/tests/coercions.ma index aec51ae8b..5429b1f82 100644 --- a/helm/matita/tests/coercions.ma +++ b/helm/matita/tests/coercions.ma @@ -36,9 +36,9 @@ let rec pos2nat x \def definition nat2int \def \lambda x. positive x. -coercion pos2nat. +coercion cic:/matita/tests/coercions/pos2nat.con. -coercion nat2int. +coercion cic:/matita/tests/coercions/nat2int.con. definition fst \def \lambda x,y:int.x. @@ -61,4 +61,4 @@ definition double2: \def \lambda f:int \to int. \lambda x : pos .f (nat2int (pos2nat x)). - \ No newline at end of file + -- 2.39.2