From 5322d66340d43e85b85e15dddcddeff3ae3a3552 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 28 Oct 2008 22:23:47 +0000 Subject: [PATCH] even more polymorphic dualizer --- .../matita/contribs/dama/dama/lebesgue.ma | 8 --- .../contribs/dama/dama/nat_ordered_set.ma | 2 +- .../matita/contribs/dama/dama/ordered_set.ma | 16 +++--- .../dama/dama/property_exhaustivity.ma | 17 ++---- .../matita/contribs/dama/dama/supremum.ma | 55 ++++++++++++------- 5 files changed, 49 insertions(+), 49 deletions(-) diff --git a/helm/software/matita/contribs/dama/dama/lebesgue.ma b/helm/software/matita/contribs/dama/dama/lebesgue.ma index 5957235cc..1536476b0 100644 --- a/helm/software/matita/contribs/dama/dama/lebesgue.ma +++ b/helm/software/matita/contribs/dama/dama/lebesgue.ma @@ -59,14 +59,6 @@ cases (wloss_prop (os_l C))(W W); unfold os_r; unfold dual_hos; simplify;rewrite rewrite Type; - wloss: ∀A:Type. (A → A → CProp) → A → A → CProp; - wloss_prop: (∀T,P,x,y.P x y = wloss T P x y) ∨ (∀T,P,x,y.P y x = wloss T P x y); + wloss: ∀A,B:Type. (A → A → B) → A → A → B; + wloss_prop: (∀T,R,P,x,y.P x y = wloss T R P x y) ∨ (∀T,R,P,x,y.P y x = wloss T R P x y); hos_excess_: hos_carr → hos_carr → CProp; - hos_coreflexive: coreflexive ? (wloss ? hos_excess_); - hos_cotransitive: cotransitive ? (wloss ? hos_excess_) + hos_coreflexive: coreflexive ? (wloss ?? hos_excess_); + hos_cotransitive: cotransitive ? (wloss ?? hos_excess_) }. -definition hos_excess ≝ λO:half_ordered_set.wloss O ? (hos_excess_ O). +definition hos_excess ≝ λO:half_ordered_set.wloss O ?? (hos_excess_ O). (* lemma find_leq : half_ordered_set → half_ordered_set. @@ -55,7 +55,7 @@ qed. definition dual_hos : half_ordered_set → half_ordered_set. intro; constructor 1; [ apply (hos_carr h); -| apply (λT,f,x,y.wloss h T f y x); +| apply (λT,R,f,x,y.wloss h T R f y x); | intros; cases (wloss_prop h);[right|left]intros;apply H; | apply (hos_excess_ h); | apply (hos_coreflexive h); @@ -169,12 +169,12 @@ apply (mk_half_ordered_set (O × O)); [1: apply (wloss O); |2: intros; cases (wloss_prop O); [left|right] intros; apply H; |3: apply (square_exc O); -|4: intro x; cases (wloss_prop O); rewrite < (H ? (square_exc O) x x); clear H; +|4: intro x; cases (wloss_prop O); rewrite < (H ?? (square_exc O) x x); clear H; cases x; clear x; unfold square_exc; intro H; cases H; clear H; simplify in H1; [1,3: apply (hos_coreflexive O h H1); |*: apply (hos_coreflexive O h1 H1);] |5: intros 3 (x0 y0 z0); cases (wloss_prop O); - do 3 rewrite < (H ? (square_exc O)); clear H; cases x0; cases y0; cases z0; clear x0 y0 z0; + do 3 rewrite < (H ?? (square_exc O)); clear H; cases x0; cases y0; cases z0; clear x0 y0 z0; simplify; intro H; cases H; clear H; [1: cases (hos_cotransitive ? h h2 h4 H1); [left;left|right;left] assumption; |2: cases (hos_cotransitive ? h1 h3 h5 H1); [left;right|right;right] assumption; diff --git a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma index 48551f85e..9788d4d35 100644 --- a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma +++ b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma @@ -19,10 +19,10 @@ lemma h_segment_upperbound: ∀C:half_ordered_set. ∀s:segment C. ∀a:sequence (half_segment_ordered_set C s). - (seg_u C s) (upper_bound ? ⌊n,\fst (a n)⌋). -intros; cases (wloss_prop C); unfold; rewrite < H; simplify; intro n; -cases (a n); simplify; unfold in H1; rewrite < H in H1; cases H1; -simplify in H2 H3; rewrite < H in H2 H3; assumption; + upper_bound ? ⌊n,\fst (a n)⌋ (seg_u C s). +intros 4; simplify; cases (a n); simplify; unfold in H; +cases (wloss_prop C); rewrite < H1 in H; simplify; cases H; +assumption; qed. notation "'segment_upperbound'" non associative with precedence 90 for @{'segment_upperbound}. @@ -68,12 +68,7 @@ definition exhaustive ≝ (a is_increasing → a is_upper_located → a is_cauchy) ∧ (b is_decreasing → b is_lower_located → b is_cauchy). -lemma prove_in_segment: - ∀O:half_ordered_set.∀s:segment O.∀x:O. - seg_l O s (λl.l ≤≤ x) → seg_u O s (λu.x ≤≤ u) → x ∈ s. -intros; unfold; cases (wloss_prop O); rewrite < H2; -split; assumption; -qed. +STOP lemma h_uparrow_to_in_segment: ∀C:half_ordered_set. @@ -83,7 +78,7 @@ lemma h_uparrow_to_in_segment: ∀x:C. uparrow C a x → in_segment C s x. intros (C H a H1 x H2); unfold in H2; cases H2; clear H2;unfold in H3 H4; cases H4; clear H4; unfold in H2; -cases (wloss_prop C) (W W); apply prove_in_segment; unfold; rewrite "𝕦_term 90 s p" non associative with precedence 45 for @{'upp $s $p}. -notation "𝕦 \sub term 90 s p" non associative with precedence 45 for @{'upp $s $p}. -notation > "𝕝_term 90 s p" non associative with precedence 45 for @{'low $s $p}. -notation "𝕝 \sub term 90 s p" non associative with precedence 45 for @{'low $s $p}. +notation > "𝕦_term 90 s" non associative with precedence 45 for @{'upp $s}. +notation "𝕦 \sub term 90 s" non associative with precedence 45 for @{'upp $s}. +notation > "𝕝_term 90 s" non associative with precedence 45 for @{'low $s}. +notation "𝕝 \sub term 90 s" non associative with precedence 45 for @{'low $s}. definition seg_u ≝ - λO:half_ordered_set.λs:segment O.λP: O → CProp. - wloss O ? (λl,u.P l) (seg_u_ ? s) (seg_l_ ? s). + λO:half_ordered_set.λs:segment O. + wloss O ?? (λl,u.l) (seg_u_ ? s) (seg_l_ ? s). definition seg_l ≝ - λO:half_ordered_set.λs:segment O.λP: O → CProp. - wloss O ? (λl,u.P l) (seg_l_ ? s) (seg_u_ ? s). + λO:half_ordered_set.λs:segment O. + wloss O ?? (λl,u.l) (seg_l_ ? s) (seg_u_ ? s). -interpretation "uppper" 'upp s P = (seg_u (os_l _) s P). -interpretation "lower" 'low s P = (seg_l (os_l _) s P). -interpretation "uppper dual" 'upp s P = (seg_l (os_r _) s P). -interpretation "lower dual" 'low s P = (seg_u (os_r _) s P). +interpretation "uppper" 'upp s = (seg_u (os_l _) s). +interpretation "lower" 'low s = (seg_l (os_l _) s). +interpretation "uppper dual" 'upp s = (seg_l (os_r _) s). +interpretation "lower dual" 'low s = (seg_u (os_r _) s). definition in_segment ≝ λO:half_ordered_set.λs:segment O.λx:O. - wloss O ? (λp1,p2.p1 ∧ p2) (seg_l ? s (λl.l ≤≤ x)) (seg_u ? s (λu.x ≤≤ u)). + wloss O ?? (λp1,p2.p1 ∧ p2) (seg_l ? s ≤≤ x) (x ≤≤ seg_u ? s). notation "‡O" non associative with precedence 90 for @{'segment $O}. interpretation "Ordered set sergment" 'segment x = (segment x). @@ -234,19 +234,19 @@ definition segment_ordered_set_exc ≝ λO:half_ordered_set.λs:‡O. λx,y:segment_ordered_set_carr O s.hos_excess_ O (\fst x) (\fst y). lemma segment_ordered_set_corefl: - ∀O,s. coreflexive ? (wloss O ? (segment_ordered_set_exc O s)). + ∀O,s. coreflexive ? (wloss O ?? (segment_ordered_set_exc O s)). intros 3; cases x; cases (wloss_prop O); generalize in match (hos_coreflexive O w); -rewrite < (H1 ? (segment_ordered_set_exc O s)); -rewrite < (H1 ? (hos_excess_ O)); intros; assumption; +rewrite < (H1 ?? (segment_ordered_set_exc O s)); +rewrite < (H1 ?? (hos_excess_ O)); intros; assumption; qed. lemma segment_ordered_set_cotrans : - ∀O,s. cotransitive ? (wloss O ? (segment_ordered_set_exc O s)). + ∀O,s. cotransitive ? (wloss O ?? (segment_ordered_set_exc O s)). intros 5 (O s x y z); cases x; cases y ; cases z; clear x y z; generalize in match (hos_cotransitive O w w1 w2); cases (wloss_prop O); -do 3 rewrite < (H3 ? (segment_ordered_set_exc O s)); -do 3 rewrite < (H3 ? (hos_excess_ O)); intros; apply H4; assumption; +do 3 rewrite < (H3 ?? (segment_ordered_set_exc O s)); +do 3 rewrite < (H3 ?? (hos_excess_ O)); intros; apply H4; assumption; qed. lemma half_segment_ordered_set: @@ -278,6 +278,19 @@ interpretation "Ordered set segment" 'segset s = (segment_ordered_set _ s). intros; try reflexivity; *) +lemma prove_in_segment: + ∀O:half_ordered_set.∀s:segment O.∀x:O. + (seg_l O s) ≤≤ x → x ≤≤ (seg_u O s) → x ∈ s. +intros; unfold; cases (wloss_prop O); rewrite < H2; +split; assumption; +qed. + +lemma cases_in_segment: + ∀C:half_ordered_set.∀s:segment C.∀x. x ∈ s → (seg_l C s) ≤≤ x ∧ x ≤≤ (seg_u C s). +intros; unfold in H; cases (wloss_prop C) (W W); rewrite