From fbfc3e402894a89b22f57e12b53e090f843a690a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 16 Nov 2007 20:49:49 +0000 Subject: [PATCH] Some notes for Enrico. --- matita/dama/excedence.ma | 12 +++++++----- matita/dama/ordered_groups.ma | 4 +++- 2 files changed, 10 insertions(+), 6 deletions(-) diff --git a/matita/dama/excedence.ma b/matita/dama/excedence.ma index 735fe2262..950639fed 100644 --- a/matita/dama/excedence.ma +++ b/matita/dama/excedence.ma @@ -21,7 +21,7 @@ include "constructive_higher_order_relations.ma". record excedence : Type ≝ { exc_carr:> Type; - exc_relation: exc_carr → exc_carr → Prop; + exc_relation: exc_carr → exc_carr → Type; (* Big bug: era in Prop!!! *) exc_coreflexive: coreflexive ? exc_relation; exc_cotransitive: cotransitive ? exc_relation }. @@ -63,7 +63,7 @@ intros (E); apply (mk_apartness E (apart E)); intros (H1); apply (H x); cases H1; assumption; |2: unfold; intros(x y H); cases H; clear H; [right|left] assumption; |3: intros (E); unfold; cases E (T f _ cTf); simplify; intros (x y z Axy); - cases Axy (H); lapply (cTf ? ? z H) as H1; cases H1; clear Axy H1; + cases Axy (H H); lapply (cTf ? ? z H) as H1; cases H1; clear Axy H1; [left; left|right; left|right; right|left; right] assumption] qed. @@ -127,12 +127,14 @@ intros (E a b Lab); cases Lab (LEab Aab); cases Aab (H H); [cases (LEab H)] fold normalize (b ≰ a); assumption; (* BUG *) qed. +(* CSC: lo avevi gia' dimostrato; ho messo apply! *) theorem le_le_to_eq: ∀E:excedence.∀x,y:E. x ≤ y → y ≤ x → x ≈ y. -intros 6 (E x y L1 L2 H); cases H; [apply (L1 H1)|apply (L2 H1)] +apply le_antisymmetric; qed. +(* CSC: perche' quel casino: bastava intros; assumption! *) lemma unfold_apart: ∀E:excedence. ∀x,y:E. x ≰ y ∨ y ≰ x → x # y. -unfold apart_of_excedence; unfold apart; simplify; intros; assumption; +intros; assumption; qed. lemma le_rewl: ∀E:excedence.∀z,y,x:E. x ≈ y → x ≤ z → y ≤ z. @@ -153,4 +155,4 @@ qed. lemma ap_rewr: ∀A:apartness.∀x,z,y:A. x ≈ y → z # y → z # x. intros (A x z y Exy Azy); apply ap_symmetric; apply (ap_rewl ???? Exy); apply ap_symmetric; assumption; -qed. +qed. \ No newline at end of file diff --git a/matita/dama/ordered_groups.ma b/matita/dama/ordered_groups.ma index cff205ce9..cc7e73928 100644 --- a/matita/dama/ordered_groups.ma +++ b/matita/dama/ordered_groups.ma @@ -32,7 +32,9 @@ qed. coercion cic:/matita/ordered_groups/og_abelian_group.con. - +(* CSC: NO! Cosi' e' nel frammento negativo. Devi scriverlo con l'eccedenza! + Tutto il resto del file e' da rigirare nel frammento positivo. +*) record ogroup : Type ≝ { og_carr:> pre_ogroup; fle_plusr: ∀f,g,h:og_carr. f≤g → f+h≤g+h -- 2.39.2