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;
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.
+ (∀y1,x1:eb. (?(ap_apart sl)) y1 x1 → y1 ≰ x1 ∨ x1 ≰ y1) →
+ (∀y2,x2:eb.y2 ≰ x2 ∨ x2 ≰ y2 → (?(ap_apart sl)) y2 x2) →
+ (∀x3,y3:eb.(le eb) x3 y3 → (?(ap_apart sl)) x3 ((?(sl_meet sl)) x3 y3)) →
+ (∀x4,y4:eb.(le eb) ((?(sl_meet sl)) x4 y4) y4) →
+ semi_lattice.
+[2,3,7,9,10: apply Type|4:apply (exc_carr eb);
+|1,5,6,8,11: intro f; cases p; apply f;]
+intros (sl eb H H1 H2 H3 H4); apply (subst_excess sl);
+ [apply (subst_excess_ sl);
+ [apply (subst_dual_excess sl);
+ [apply (subst_excess_base sl eb);
+ |apply H;]
+ | (*clear H2 H3 H4;*)
+ change in ⊢ (% -> % -> ?) with (exc_carr eb);
+ unfold subst_excess_base; unfold mk_excess_dual_smart;
+ unfold subst_dual_excess; simplify in ⊢ (?→?→?→%);
+ (unfold exc_ap; simplify in ⊢ (?→?→? % ? ?→?));
+ simplify; intros (x y H2); apply H1;
+ generalize in match H2;
+ generalize in match x as x;
+ generalize in match y as y; (*clear H1 H2 x y;*)
+ change in ⊢ (?→?→match ? return λ_:?.(λ_:? ? % ?.?) with [_⇒?] ? ?→?)
+ with (Type_OF_semi_lattice sl);
+ change in ⊢ (?→?→match match ? return λ_:?.(λ_:? ? % ?.? ? % ?) with [_⇒? ? %] return ? with [_⇒?] ??→?) with (Type_OF_semi_lattice sl);
+ cases H; intros; assumption; (* se faccio le clear... BuM! *)
+ | clear H1 H3 H4;
+
+ ]
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: latt_jcarr_ = subst latt_jcarr (exc_dual_dual 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 =
projects / helm.git / blobdiff