From 2de5506abeebb60e552d68b828d8c481ee7be742 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 31 Jan 2008 12:43:37 +0000 Subject: [PATCH] snapshot --- helm/software/matita/dama/TODO | 2 + helm/software/matita/dama/excess.ma | 85 +++++--- helm/software/matita/dama/lattice.ma | 299 ++++++++++++++++++++++++++- 3 files changed, 347 insertions(+), 39 deletions(-) diff --git a/helm/software/matita/dama/TODO b/helm/software/matita/dama/TODO index 6e2ccdd68..353329bea 100644 --- a/helm/software/matita/dama/TODO +++ b/helm/software/matita/dama/TODO @@ -1,2 +1,4 @@ changing file resets the display-notation ref, but not the GUI tick mettere una maction in tutti i body (ma forse non basta) +la visualizzazione dellea notazione se viene disttivata e poi se ne definisce una... la rende causa +il fatto che disabilitarla significa rimuovere quelle definite fino ad ora, non disabilitarla in senso proprio. diff --git a/helm/software/matita/dama/excess.ma b/helm/software/matita/dama/excess.ma index 826ae8c0b..9068d297b 100644 --- a/helm/software/matita/dama/excess.ma +++ b/helm/software/matita/dama/excess.ma @@ -26,7 +26,32 @@ record excess_base : Type ≝ { exc_cotransitive: cotransitive ? exc_excess }. -interpretation "excess" 'nleq a b = (cic:/matita/excess/exc_excess.con _ a b). +interpretation "Excess base excess" 'nleq a b = (cic:/matita/excess/exc_excess.con _ a b). + +(* E(#,≰) → E(#,sym(≰)) *) +lemma make_dual_exc: excess_base → excess_base. +intro E; +apply (mk_excess_base (exc_carr E)); + [ apply (λx,y:E.y≰x);|apply exc_coreflexive; + | unfold cotransitive; simplify; intros (x y z H); + cases (exc_cotransitive E ??z H);[right|left]assumption] +qed. + +record excess_dual : Type ≝ { + exc_dual_base:> excess_base; + exc_dual_dual_ : excess_base; + exc_with: exc_dual_dual_ = make_dual_exc exc_dual_base +}. + +lemma mk_excess_dual_smart: excess_base → excess_dual. +intro; apply mk_excess_dual; [apply e| apply (make_dual_exc e)|reflexivity] +qed. + +definition exc_dual_dual: excess_dual → excess_base. +intro E; apply (make_dual_exc E); +qed. + +coercion cic:/matita/excess/exc_dual_dual.con. record apartness : Type ≝ { ap_carr:> Type; @@ -50,32 +75,44 @@ intros (E); apply (mk_apartness E (λa,b:E. a ≰ b ∨ b ≰ a)); qed. record excess_ : Type ≝ { - exc_exc:> excess_base; + exc_exc:> excess_dual; exc_ap_: apartness; - exc_with: ap_carr exc_ap_ = exc_carr exc_exc + exc_with1: ap_carr exc_ap_ = exc_carr exc_exc }. definition exc_ap: excess_ → apartness. intro E; apply (mk_apartness E); unfold Type_OF_excess_; -cases (exc_with E); simplify; +cases (exc_with1 E); simplify; [apply (ap_apart (exc_ap_ E)); |apply ap_coreflexive;|apply ap_symmetric;|apply ap_cotransitive] qed. coercion cic:/matita/excess/exc_ap.con. +interpretation "Excess excess_" 'nleq a b = + (cic:/matita/excess/exc_excess.con (cic:/matita/excess/excess_base_OF_excess_1.con _) a b). + record excess : Type ≝ { excess_carr:> excess_; ap2exc: ∀y,x:excess_carr. y # x → y ≰ x ∨ x ≰ y; exc2ap: ∀y,x:excess_carr.y ≰ x ∨ x ≰ y → y # x }. +interpretation "Excess excess" 'nleq a b = + (cic:/matita/excess/exc_excess.con (cic:/matita/excess/excess_base_OF_excess1.con _) a b). + +interpretation "Excess (dual) excess" 'ngeq a b = + (cic:/matita/excess/exc_excess.con (cic:/matita/excess/excess_base_OF_excess.con _) a b). + definition strong_ext ≝ λA:apartness.λop:A→A.∀x,y. op x # op y → x # y. -definition le ≝ λE:excess.λa,b:E. ¬ (a ≰ b). +definition le ≝ λE:excess_base.λa,b:E. ¬ (a ≰ b). -interpretation "ordered sets less or equal than" 'leq a b = - (cic:/matita/excess/le.con _ a b). +interpretation "Excess less or equal than" 'leq a b = + (cic:/matita/excess/le.con (cic:/matita/excess/excess_base_OF_excess1.con _) a b). + +interpretation "Excess less or equal than" 'geq a b = + (cic:/matita/excess/le.con (cic:/matita/excess/excess_base_OF_excess.con _) a b). lemma le_reflexive: ∀E.reflexive ? (le E). unfold reflexive; intros 3 (E x H); apply (exc_coreflexive ?? H); @@ -89,14 +126,15 @@ qed. definition eq ≝ λA:apartness.λa,b:A. ¬ (a # b). notation "hvbox(a break ≈ b)" non associative with precedence 50 for @{ 'napart $a $b}. -interpretation "alikeness" 'napart a b = - (cic:/matita/excess/eq.con _ a b). +interpretation "Apartness alikeness" 'napart a b = (cic:/matita/excess/eq.con _ a b). +interpretation "Excess alikeness" 'napart a b = (cic:/matita/excess/eq.con (cic:/matita/excess/excess_base_OF_excess1.con _) a b). +interpretation "Excess (dual) alikeness" 'napart a b = (cic:/matita/excess/eq.con (cic:/matita/excess/excess_base_OF_excess.con _) a b). -lemma eq_reflexive:∀E. reflexive ? (eq E). +lemma eq_reflexive:∀E:apartness. reflexive ? (eq E). intros (E); unfold; intros (x); apply ap_coreflexive; qed. -lemma eq_sym_:∀E.symmetric ? (eq E). +lemma eq_sym_:∀E:apartness.symmetric ? (eq E). unfold symmetric; intros 5 (E x y H H1); cases (H (ap_symmetric ??? H1)); qed. @@ -105,7 +143,7 @@ lemma eq_sym:∀E:apartness.∀x,y:E.x ≈ y → y ≈ x ≝ eq_sym_. (* SETOID REWRITE *) coercion cic:/matita/excess/eq_sym.con. -lemma eq_trans_: ∀E.transitive ? (eq E). +lemma eq_trans_: ∀E:apartness.transitive ? (eq E). (* bug. intros k deve fare whd quanto basta *) intros 6 (E x y z Exy Eyz); intro Axy; cases (ap_cotransitive ???y Axy); [apply Exy|apply Eyz] assumption. @@ -118,7 +156,8 @@ notation > "'Eq'≈" non associative with precedence 50 for @{'eqrewrite}. interpretation "eq_rew" 'eqrewrite = (cic:/matita/excess/eq_trans.con _ _ _). alias id "antisymmetric" = "cic:/matita/constructive_higher_order_relations/antisymmetric.con". -lemma le_antisymmetric: ∀E.antisymmetric ? (le E) (eq ?). +lemma le_antisymmetric: + ∀E:excess.antisymmetric ? (le (excess_base_OF_excess1 E)) (eq E). intros 5 (E x y Lxy Lyx); intro H; cases (ap2exc ??? H); [apply Lxy;|apply Lyx] assumption; qed. @@ -136,8 +175,8 @@ lemma lt_transitive: ∀E.transitive ? (lt E). intros (E); unfold; intros (x y z H1 H2); cases H1 (Lxy Axy); cases H2 (Lyz Ayz); split; [apply (le_transitive ???? Lxy Lyz)] clear H1 H2; elim (ap2exc ??? Axy) (H1 H1); elim (ap2exc ??? Ayz) (H2 H2); [1:cases (Lxy H1)|3:cases (Lyz H2)] -clear Axy Ayz;lapply (exc_cotransitive E) as c; unfold cotransitive in c; -lapply (exc_coreflexive E) as r; unfold coreflexive in r; +clear Axy Ayz;lapply (exc_cotransitive (exc_dual_base E)) as c; unfold cotransitive in c; +lapply (exc_coreflexive (exc_dual_base E)) as r; unfold coreflexive in r; [1: lapply (c ?? y H1) as H3; elim H3 (H4 H4); [cases (Lxy H4)|cases (r ? H4)] |2: lapply (c ?? x H2) as H3; elim H3 (H4 H4); [apply exc2ap; right; assumption|cases (Lxy H4)]] qed. @@ -177,6 +216,7 @@ interpretation "ap_rewl" 'aprewritel = (cic:/matita/excess/ap_rewl.con _ _ _). notation > "'Ap'≫" non associative with precedence 50 for @{'aprewriter}. interpretation "ap_rewr" 'aprewriter = (cic:/matita/excess/ap_rewr.con _ _ _). +alias symbol "napart" = "Apartness alikeness". lemma exc_rewl: ∀A:excess.∀x,z,y:A. x ≈ y → y ≰ z → x ≰ z. intros (A x z y Exy Ayz); elim (exc_cotransitive ???x Ayz); [2:assumption] cases Exy; apply exc2ap; right; assumption; @@ -237,18 +277,3 @@ qed. definition total_order_property : ∀E:excess. Type ≝ λE:excess. ∀a,b:E. a ≰ b → b < a. -(* E(#,≰) → E(#,sym(≰)) *) -lemma dual_exc: excess→ excess. -intro E; apply mk_excess; -[1: apply mk_excess_; - [1: apply (mk_excess_base (exc_carr (excess_carr E))); - [ apply (λx,y:E.y≰x);|apply exc_coreflexive; - | unfold cotransitive; simplify; intros (x y z H); - cases (exc_cotransitive E ??z H);[right|left]assumption] - |2: apply (exc_ap_ E); - |3: apply (exc_with E);] -|2: simplify; intros (y x H); fold simplify (y#x) in H; - apply ap2exc; apply ap_symmetric; apply H; -|3: simplify; intros; fold simplify (y#x); apply exc2ap; - cases o; [right|left]assumption] -qed. diff --git a/helm/software/matita/dama/lattice.ma b/helm/software/matita/dama/lattice.ma index ef0213425..79bc27ee1 100644 --- a/helm/software/matita/dama/lattice.ma +++ b/helm/software/matita/dama/lattice.ma @@ -30,8 +30,8 @@ lemma excess_of_semi_lattice_base: semi_lattice_base → excess. intro l; apply mk_excess; [1: apply mk_excess_; - [1: - + [1: apply mk_excess_dual_smart; + apply (mk_excess_base (sl_carr l)); [1: apply (λa,b:sl_carr l.a # (a ✗ b)); |2: unfold; intros 2 (x H); simplify in H; @@ -161,22 +161,303 @@ unfold excl; simplify; qed. *) +(* ED(≰,≱) → EB(≰') → ED(≰',≱') *) +lemma subst_excess_base: excess_dual → excess_base → excess_dual. +intros; apply (mk_excess_dual_smart e1); +qed. + +(* E_(ED(≰,≱),AP(#),c ED = c AP) → ED' → c DE' = c E_ → E_(ED',#,p) *) +lemma subst_dual_excess: ∀e:excess_.∀e1:excess_dual.exc_carr e = exc_carr e1 → excess_. +intros (e e1 p); apply (mk_excess_ e1 e); cases p; reflexivity; +qed. + +(* E(E_,H1,H2) → E_' → H1' → H2' → E(E_',H1',H2') *) +alias symbol "nleq" = "Excess excess_". +lemma subst_excess_: ∀e:excess. ∀e1:excess_. + (∀y,x:e1. y # x → y ≰ x ∨ x ≰ y) → + (∀y,x:e1.y ≰ x ∨ x ≰ y → y # x) → + excess. +intros (e e1 H1 H2); apply (mk_excess e1 H1 H2); +qed. + +(* SL(E,M,H2-5(#),H67(≰)) → E' → c E = c E' → H67'(≰') → SL(E,M,p2-5,H67') *) +lemma subst_excess: + ∀l:semi_lattice. + ∀e:excess. + ∀p:exc_ap l = exc_ap e. + (∀x,y:e.(le (exc_dual_base e)) x y → x ≈ (?(sl_meet l)) x y) → + (∀x,y:e.(le (exc_dual_base e)) ((?(sl_meet l)) x y) y) → + semi_lattice. +[1,2:intro M; + change with ((λx.ap_carr x) e -> (λx.ap_carr x) e -> (λx.ap_carr x) e); + cases p; apply M; +|intros (l e p H1 H2); + apply (mk_semi_lattice e); + [ change with ((λx.ap_carr x) e -> (λx.ap_carr x) e -> (λx.ap_carr x) e); + cases p; simplify; apply (sl_meet l); + |2: change in ⊢ (% → ?) with ((λx.ap_carr x) e); cases p; simplify; apply sl_meet_refl; + |3: change in ⊢ (% → % → ?) with ((λx.ap_carr x) e); cases p; simplify; apply sl_meet_comm; + |4: change in ⊢ (% → % → % → ?) with ((λx.ap_carr x) e); cases p; simplify; apply sl_meet_assoc; + |5: change in ⊢ (% → ?) with ((λx.ap_carr x) e); cases p; simplify; apply sl_strong_extm; + |6: clear H2; apply H1; + |7: clear H1; apply H2;]] +qed. + +lemma excess_of_excess_base: excess_base → excess. +intro eb; +apply mk_excess; + [apply (mk_excess_ (mk_excess_dual_smart eb)); + [apply (apartness_of_excess_base eb); + |reflexivity] + |2,3: intros; assumption] +qed. + +lemma subst_excess_base_in_semi_lattice: + ∀sl:semi_lattice. + ∀eb:excess_base. + ∀p:exc_carr sl = exc_carr eb. + + mancano le 4 proprietà riscritte con p + + semi_lattice. +intros (l eb H); apply (subst_excess l); + [apply (subst_excess_ l); + [apply (subst_dual_excess l); + [apply (subst_excess_base l eb); + |apply H;] + | change in \vdash (% -> % -> ?) with (exc_carr eb); + letin xxx \def (ap2exc l); clearbody xxx; + change in xxx:(%→%→?) with (Type_OF_semi_lattice l); + whd in ⊢ (?→?→? (? %) ? ?→?); + unfold exc_ap; + simplify in ⊢ (?→?→%→?); + +intros 2; +generalize in ⊢ (% -> ?); intro P; +generalize in match x in ⊢ % as x; +generalize in match y in ⊢ % as y; clear x y; + + +cases H; simplify; + + +cut (Πy:exc_carr eb +.Πx:exc_carr eb + .match  + (match H +  in eq +  return  + λright_1:Type + .(λmatched:eq Type (Type_OF_excess_ (excess__OF_semi_lattice l)) right_1 + .eq Type (Type_OF_excess_ (excess__OF_semi_lattice l)) right_1) +  with  + [refl_eq⇒refl_eq Type (Type_OF_excess_ (excess__OF_semi_lattice l))]) +  in eq +  return  + λright_1:Type + .(λmatched:eq Type (ap_carr (exc_ap (excess__OF_semi_lattice l))) right_1 + .right_1→right_1→Type) +  with  + [refl_eq⇒ap_apart (exc_ap (excess__OF_semi_lattice l))] y x);[2: + + + change in ⊢ (?→?→? % ? ?→?) with (exc_ap_ (excess__OF_semi_lattice l)); + generalize in match H in \vdash (? -> %); cases H; + cases H; + + +normalize in ⊢ (?→?→?→? (? (? (? ? (% ? ?) ?)) ? ?) ?); +whd in ⊢ (?→?→? % ? ?→?); change in ⊢ (?→?→? (? % ? ? ? ?) ? ?→?) with (exc_carr eb); +cases H; + change in ⊢ (?→?→? % ? ?→?) with (exc_ap l); +(subst_dual_excess (excess__OF_semi_lattice l) + (subst_excess_base (excess_dual_OF_semi_lattice l) eb) H) + + + unfold subst_excess_base; + unfold mk_excess_dual_smart; + unfold excess__OF_semi_lattice; + unfold excess_dual_OF_semi_lattice; + unfold excess_dual_OF_semi_lattice; + + reflexivity] +*) record lattice_ : Type ≝ { latt_mcarr:> semi_lattice; latt_jcarr_: semi_lattice; - latt_with: sl_exc latt_jcarr_ = dual_exc (sl_exc latt_mcarr) +(* latt_with1: (subst_excess_ + (subst_dual_excess + (subst_excess_base + (excess_dual_OF_excess (sl_exc latt_jcarr_)) + (excess_base_OF_excess (sl_exc latt_mcarr))))) = + sl_exc latt_jcarr_; + +*) + latt_with1: excess_base_OF_excess1 (sl_exc latt_jcarr_) = excess_base_OF_excess (sl_exc latt_mcarr); + latt_with2: excess_base_OF_excess (sl_exc latt_jcarr_) = excess_base_OF_excess1 (sl_exc latt_mcarr); + latt_with3: apartness_OF_excess (sl_exc latt_jcarr_) = apartness_OF_excess (sl_exc latt_mcarr) }. +axiom FALSE: False. + lemma latt_jcarr : lattice_ → semi_lattice. intro l; -apply (mk_semi_lattice (dual_exc l)); -unfold excess_OF_lattice_; -cases (latt_with l); simplify; -[apply sl_meet|apply sl_meet_refl|apply sl_meet_comm|apply sl_meet_assoc| -apply sl_strong_extm| apply sl_le_to_eqm|apply sl_lem] -qed. +apply mk_semi_lattice; + [apply mk_excess; + [apply mk_excess_; + [apply (mk_excess_dual_smart l); + |apply (exc_ap l); + |reflexivity] + |unfold mk_excess_dual_smart; simplify; + intros (x y H); cases (ap2exc ??? H); [right|left] assumption; + |unfold mk_excess_dual_smart; simplify; + intros (x y H);cases H; apply exc2ap;[right|left] assumption;]] +unfold mk_excess_dual_smart; simplify; +[1: change with ((λx.ap_carr x) l → (λx.ap_carr x) l → (λx.ap_carr x) l); + simplify; unfold apartness_OF_lattice_; + cases (latt_with3 l); apply (sl_meet (latt_jcarr_ l)); +|2: change in ⊢ (%→?) with ((λx.ap_carr x) l); simplify; + unfold apartness_OF_lattice_; + cases (latt_with3 l); apply (sl_meet_refl (latt_jcarr_ l)); +|3: change in ⊢ (%→%→?) with ((λx.ap_carr x) l); simplify; unfold apartness_OF_lattice_; + cases (latt_with3 l); apply (sl_meet_comm (latt_jcarr_ l)); +|4: change in ⊢ (%→%→%→?) with ((λx.ap_carr x) l); simplify; unfold apartness_OF_lattice_; + cases (latt_with3 l); apply (sl_meet_assoc (latt_jcarr_ l)); +|5: change in ⊢ (%→%→%→?) with ((λx.ap_carr x) l); simplify; unfold apartness_OF_lattice_; + cases (latt_with3 l); apply (sl_strong_extm (latt_jcarr_ l)); +|7: +(* +unfold excess_base_OF_lattice_; + change in ⊢ (?→?→? ? (% ? ?) ?) + with (match latt_with3 l + in eq + return  +λright_1:apartness +.(λmatched:eq apartness (apartness_OF_semi_lattice (latt_jcarr_ l)) right_1 + .ap_carr right_1→ap_carr right_1→ap_carr right_1) + with  +[refl_eq⇒sl_meet (latt_jcarr_ l)] + : ? +); + change in ⊢ (?→?→? ? ((?:%->%->%) ? ?) ?) + with ((λx.exc_carr x) (excess_base_OF_semi_lattice (latt_mcarr l))); + unfold excess_base_OF_lattice_ in ⊢ (?→?→? ? ((?:%->%->%) ? ?) ?); + simplify in ⊢ (?→?→? ? ((?:%->%->%) ? ?) ?); +change in ⊢ (?→?→? ? (% ? ?) ?) with + (match refl_eq ? (excess__OF_semi_lattice (latt_mcarr l)) in eq + return (λR.λE:eq ? (excess_base_OF_semi_lattice (latt_mcarr l)) R.R → R → R) + with [refl_eq⇒ + (match latt_with3 l in eq +  return  + (λright:apartness + .(λmatched:eq apartness (apartness_OF_semi_lattice (latt_jcarr_ l)) right + .ap_carr right→ap_carr right→ap_carr right)) +  with [refl_eq⇒ sl_meet (latt_jcarr_ l)] +  : +  exc_carr (excess_base_OF_semi_lattice (latt_mcarr l)) + →exc_carr (excess_base_OF_semi_lattice (latt_mcarr l)) + →exc_carr (excess_base_OF_semi_lattice (latt_mcarr l)) +  ) + ]); + generalize in ⊢ (?→?→? ? (match % return ? with [_⇒?] ? ?) ?); + unfold excess_base_OF_lattice_ in ⊢ (? ? ? %→?); + cases (latt_with1 l); + change in ⊢ (?→?→?→? ? (match ? return ? with [_⇒(?:%→%->%)] ? ?) ?) + with ((λx.ap_carr x) (latt_mcarr l)); + simplify in ⊢ (?→?→?→? ? (match ? return ? with [_⇒(?:%→%->%)] ? ?) ?); + cases (latt_with3 l); + + change in ⊢ (? ? % ?→?) with ((λx.ap_carr x) l); + simplify in ⊢ (% → ?); + change in ⊢ (?→?→?→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?) + with ((λx.ap_carr x) (apartness_OF_lattice_ l)); + unfold apartness_OF_lattice_; + cases (latt_with3 l); simplify; + change in ⊢ (? ? ? %→%→%→?) with ((λx.exc_carr x) l); + unfold excess_base_OF_lattice_; + cases (latt_with1 l); simplify; + change in \vdash (? -> % -> % -> ?) with (exc_carr (excess_base_OF_semi_lattice (latt_jcarr_ l))); + change in ⊢ ((? ? % ?)→%→%→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?) + with ((λx.exc_carr x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l))); + simplify; + intro H; + unfold excess_base_OF_semi_lattice1; + unfold excess_base_OF_excess1; + unfold excess_base_OF_excess_1; + change +*) + +change in ⊢ (?→?→? ? (% ? ?) ?) with + (match refl_eq ? (Type_OF_lattice_ l) in eq + return (λR.λE:eq ? (Type_OF_lattice_ l) R.R → R → R) + with [refl_eq⇒ + match latt_with3 l in eq +  return  + (λright:apartness + .(λmatched:eq apartness (apartness_OF_semi_lattice (latt_jcarr_ l)) right + .ap_carr right→ap_carr right→ap_carr right)) +  with [refl_eq⇒ sl_meet (latt_jcarr_ l)] + ]); + generalize in ⊢ (?→?→? ? (match % return ? with [_⇒?] ? ?) ?); + change in ⊢ (? ? % ?→?) with ((λx.ap_carr x) l); + simplify in ⊢ (% → ?); + change in ⊢ (?→?→?→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?) + with ((λx.ap_carr x) (apartness_OF_lattice_ l)); + unfold apartness_OF_lattice_; + cases (latt_with3 l); simplify; + change in ⊢ (? ? ? %→%→%→?) with ((λx.exc_carr x) l); + unfold excess_base_OF_lattice_; + cases (latt_with1 l); simplify; + change in \vdash (? -> % -> % -> ?) with (exc_carr (excess_base_OF_semi_lattice (latt_jcarr_ l))); + change in ⊢ ((? ? % ?)→%→%→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?) + with ((λx.exc_carr x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l))); + simplify; + intro H; + change in ⊢ (?→?→%) with (le (mk_excess_base + ((λx.exc_carr x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l))) + ((λx.exc_excess x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l))) + ((λx.exc_coreflexive x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l))) + ((λx.exc_cotransitive x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l))) + ) (match H + in eq + return  +λR:Type +.(λE:eq Type (exc_carr (excess_base_OF_semi_lattice1 (latt_jcarr_ l))) R + .R→R→R) + with  +[refl_eq⇒sl_meet (latt_jcarr_ l)] x y) y); + simplify in ⊢ (?→?→? (? % ???) ? ?); + change in ⊢ (?→?→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?) + with ((λx.exc_carr x) (excess_base_OF_semi_lattice1 (latt_jcarr_ l))); + simplify in ⊢ (?→?→? ? (match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?) ?); + lapply (match H in eq return + λright.λe:eq ? (exc_carr (excess_base_OF_semi_lattice1 (latt_jcarr_ l))) right. + +∀x:right +.∀y:right + .le + (mk_excess_base right ???) + (match e +  in eq +  return  + λR:Type.(λE:eq Type (exc_carr (excess_base_OF_semi_lattice1 (latt_jcarr_ l))) R.R→R→R) +  with  + [refl_eq⇒sl_meet (latt_jcarr_ l)] x y) y + with [refl_eq ⇒ ?]) as XX; + [cases e; apply (exc_excess (latt_jcarr_ l)); + |unfold;cases e;simplify;apply (exc_coreflexive (latt_jcarr_ l)); + |unfold;cases e;simplify;apply (exc_cotransitive (latt_jcarr_ l)); + ||apply XX| + |apply XX; + + simplify; apply (sl_lem); +|elim FALSE] +qed. + + + coercion cic:/matita/lattice/latt_jcarr.con. interpretation "Lattice meet" 'and a b = -- 2.39.2