intros (e e1 H1 H2); apply (mk_excess e1 H1 H2);
qed.
+definition hole ≝ λT:Type.λx:T.x.
+
+notation < "\ldots" non associative with precedence 50 for @{'hole}.
+interpretation "hole" 'hole = (cic:/matita/lattice/hole.con _ _).
+
+
+axiom FALSE : False.
+
(* SL(E,M,H2-5(#),H67(≰)) → E' → c E = c E' → H67'(≰') → SL(E,M,p2-5,H67') *)
lemma subst_excess:
∀l:semi_lattice.
|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;]]
+ |6: clear H2; apply hole; apply H1;
+ |7: clear H1; apply hole; apply H2;]]
qed.
lemma excess_of_excess_base: excess_base → excess.
|2,3: intros; assumption]
qed.
+lemma subst_excess_preserves_aprtness:
+ ∀l:semi_lattice.
+ ∀e:excess.
+ ∀p,H1,H2.
+ exc_ap l = exc_ap (subst_excess l e p H1 H2).
+intros;
+unfold subst_excess;
+simplify; assumption;
+qed.
+
+
+lemma subst_excess__preserves_aprtness:
+ ∀l:excess.
+ ∀e:excess_base.
+ ∀p,H1,H2.
+ exc_ap l = apartness_OF_excess (subst_excess_ l (subst_dual_excess l (subst_excess_base l e) p) H1 H2).
+intros 3; (unfold subst_excess_; unfold subst_dual_excess; unfold subst_excess_base; unfold exc_ap; unfold mk_excess_dual_smart; simplify);
+(unfold subst_excess_base in p; unfold mk_excess_dual_smart in p; simplify in p);
+intros; cases p;
+reflexivity;
+qed.
+
+lemma subst_excess_base_in_excess_:
+ ∀d:excess_.
+ ∀eb:excess_base.
+ ∀p:exc_carr d = exc_carr eb.
+ excess_.
+intros (e_ eb);
+apply (subst_dual_excess e_);
+ [apply (subst_excess_base e_ eb);
+ |assumption]
+qed.
+
+lemma subst_excess_base_in_excess:
+ ∀d:excess.
+ ∀eb:excess_base.
+ ∀p:exc_carr d = exc_carr eb.
+ (∀y1,x1:eb. (?(ap_apart d)) y1 x1 → y1 ≰ x1 ∨ x1 ≰ y1) →
+ (∀y2,x2:eb.y2 ≰ x2 ∨ x2 ≰ y2 → (?(ap_apart d)) y2 x2) →
+ excess.
+[1,3,4:apply Type|2,5:intro f; cases p; apply f]
+intros (d eb p H1 H2);
+apply (subst_excess_ d);
+ [apply (subst_excess_base_in_excess_ d eb p);
+ |apply hole; clear H2;
+ change in ⊢ (%→%→?) with (exc_carr eb);
+ change in ⊢ (?→?→?→? (? % ? ?) (? % ? ?)) with eb; intros (y x H3);
+ apply H1; generalize in match H3;
+ unfold ap_apart; unfold subst_excess_base_in_excess_;
+ unfold subst_dual_excess; simplify;
+ generalize in match x;
+ generalize in match y;
+ cases p; simplify; intros; assumption;
+ |apply hole; clear H1;
+ change in ⊢ (%→%→?) with (exc_carr eb);
+ change in ⊢ (?→?→? (? % ? ?) (? % ? ?)→?) with eb; intros (y x H3);
+ unfold ap_apart; unfold subst_excess_base_in_excess_;
+ unfold subst_dual_excess; simplify; generalize in match (H2 ?? H3);
+ generalize in match x; generalize in match y; cases p;
+ intros; assumption;]
+qed.
+
+lemma tech1: ∀e:excess.
+ ∀eb:excess_base.
+ ∀p,H1,H2.
+ exc_ap e = exc_ap_ (subst_excess_base_in_excess e eb p H1 H2).
+intros (e eb p H1 H2);
+unfold subst_excess_base_in_excess;
+unfold subst_excess_; simplify;
+unfold subst_excess_base_in_excess_;
+unfold subst_dual_excess; simplify; reflexivity;
+qed.
+
+lemma tech2:
+ ∀e:excess_.∀eb.∀p.
+ exc_ap e = exc_ap (mk_excess_ (subst_excess_base e eb) (exc_ap e) p).
+intros (e eb p);unfold exc_ap; simplify; cases p; simplify; reflexivity;
+qed.
+
+(*
+lemma eq_fap:
+ ∀a1,b1,a2,b2,a3,b3,a4,b4,a5,b5.
+ a1=b1 → a2=b2 → a3=b3 → a4=b4 → a5=b5 → mk_apartness a1 a2 a3 a4 a5 = mk_apartness b1 b2 b3 b4 b5.
+intros; cases H; cases H1; cases H2; cases H3; cases H4; reflexivity;
+qed.
+*)
+
+lemma subst_excess_base_in_excess_preserves_apartness:
+ ∀e:excess.
+ ∀eb:excess_base.
+ ∀H,H1,H2.
+ apartness_OF_excess e =
+ apartness_OF_excess (subst_excess_base_in_excess e eb H H1 H2).
+intros (e eb p H1 H2);
+unfold subst_excess_base_in_excess;
+unfold subst_excess_; unfold subst_excess_base_in_excess_;
+unfold subst_dual_excess; unfold apartness_OF_excess;
+simplify in ⊢ (? ? ? (? %));
+rewrite < (tech2 e eb );
+reflexivity;
+qed.
+
+
+
+alias symbol "nleq" = "Excess base excess".
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)) →
+ (∀x3,y3:eb.(le eb) x3 y3 → (?(eq 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;
-
- ]
+[2:apply Prop|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_base_in_excess sl eb H H1 H2);
+ |apply subst_excess_base_in_excess_preserves_apartness;
+ |change in ⊢ (%→%→?) with ((λx.ap_carr x) (subst_excess_base_in_excess (sl_exc sl) eb H H1 H2)); simplify;
+ intros 3 (x y LE);
+ generalize in match (H3 ?? LE);
+ generalize in match H1 as H1;generalize in match H2 as H2;
+ generalize in match x as x; generalize in match y as y;
+ cases FALSE;
+ (*
+ (reduce in H ⊢ %; cases H; simplify; intros; assumption);
+
+
+ cases (subst_excess_base_in_excess_preserves_apartness (sl_exc sl) eb H H1 H2); simplify;
+ change in x:(%) with (exc_carr eb);
+ change in y:(%) with (exc_carr eb);
+ generalize in match OK; generalize in match x as x; generalize in match y as y;
+ cases H; simplify; (* funge, ma devo fare 2 rewrite in un colpo solo *)
+ *)
+ |cases FALSE;
+ ]
+qed.
record lattice_ : Type ≝ {
latt_mcarr:> semi_lattice;
latt_jcarr_: semi_lattice;
- (*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)
+ W1:?; W2:?; W3:?; W4:?; W5:?;
+ latt_with1: latt_jcarr_ = subst_excess_base_in_semi_lattice latt_jcarr_
+ (excess_base_OF_semi_lattice latt_mcarr) W1 W2 W3 W4 W5
}.
-axiom FALSE: False.
-
lemma latt_jcarr : lattice_ → semi_lattice.
-intro l;
-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]
+intro l; apply (subst_excess_base_in_semi_lattice (latt_jcarr_ l) (excess_base_OF_semi_lattice (latt_mcarr l)) (W1 l) (W2 l) (W3 l) (W4 l) (W5 l));
qed.
-
-
-
coercion cic:/matita/lattice/latt_jcarr.con.
projects / helm.git / blobdiff