Library gaia_hydras.T1Choice
Experimental !!!! This file is a draft !!!
From mathcomp Require Import all_ssreflect zify.
From Coq Require Import Logic.Eqdep_dec.
From hydras Require Import DecPreOrder ON_Generic T1 E0.
From gaia Require Export ssete9.
From gaia_hydras Require Import T1Bridge.
Set Implicit Arguments.
Type T1 vs generic trees
Fixpoint T12Tree (a: T1): GenTree.tree nat :=
if a is cons b n c
then GenTree.Node n [:: T12Tree b; T12Tree c]
else GenTree.Leaf 0.
Fixpoint Tree2T1 (t: GenTree.tree nat): option T1 :=
match t with
| GenTree.Leaf 0 ⇒ Some zero
| GenTree.Node n [:: t1; t2] ⇒
match Tree2T1 t1, Tree2T1 t2 with
| Some b, Some c ⇒ Some (cons b n c)
| _, _ ⇒ None
end
| _ ⇒ None
end.
Lemma TreeT1K : pcancel T12Tree Tree2T1.
to remove (useless)
Lemma T12Tree_inj: injective T12Tree.
Definition T1mixin :
Countable.mixin_of T1 := PcanCountMixin TreeT1K.
Canonical T1Choice :=
Eval hnf in ChoiceType T1 (CountChoiceMixin T1mixin).
Example ex_pos: ∃ alpha: T1, zero != alpha.
Example some_pos: T1 := xchoose ex_pos.
Example some_pos' : T1 := choose (fun p : T1 ⇒ zero != p)
T1omega.
Goal (zero: T1Choice) != some_pos'.
Definition T1mixin :
Countable.mixin_of T1 := PcanCountMixin TreeT1K.
Canonical T1Choice :=
Eval hnf in ChoiceType T1 (CountChoiceMixin T1mixin).
Example ex_pos: ∃ alpha: T1, zero != alpha.
Example some_pos: T1 := xchoose ex_pos.
Example some_pos' : T1 := choose (fun p : T1 ⇒ zero != p)
T1omega.
Goal (zero: T1Choice) != some_pos'.
= EqType T1 (EqMixin (@T1eqP))
: eqType
= Choice.Pack
{|
Choice.base := EqMixin (@T1eqP);
Choice.mixin := PcanChoiceMixin (pcan_pickleK TreeT1K)
|}
: choiceType
Definition T1_le_Mixin := leOrderMixin T1Choice.
Definition T1min a b := if T1lt a b then a else b.
Definition T1max a b := if T1lt a b then b else a.
Lemma T1ltE x y : T1lt x y = (y != x) && T1le x y.
Lemma T1minE x y : T1min x y = (if T1lt x y then x else y).
Lemma T1maxE x y : T1max x y = (if T1lt x y then y else x).
Lemma T1le_asym: ssrbool.antisymmetric T1le.
Definition T1leOrderMixin : leOrderMixin T1Choice :=
LeOrderMixin T1ltE T1minE T1maxE T1le_asym T1le_trans T1le_total.
Canonical T1orderType :=
@OrderOfChoiceType tt T1Choice T1leOrderMixin.
Goal @Order.le tt T1orderType T1omega T1omega.
Check T1omega: T1orderType.
Goal ((T1omega:T1orderType) ≤ (T1omega:T1orderType))%O.
Notation "x <= y" := (@Order.le _ T1orderType x y).
Notation "x < y" := (@Order.lt _ T1orderType x y).
About Order.le.
Goal @Order.le tt T1orderType T1omega T1omega.
Import Order.POrderTheory.
Goal T1omega ≤ T1omega.
Set Printing All.
Goal T1omega < T1succ T1omega.
Goal ~~ (<%O (T1omega:T1orderType) (T1omega:T1orderType)).
Goal ~~(T1omega < T1omega).
Goal ~~ @Order.lt tt (T1orderType) T1omega T1omega.
Goal T1omega ≤ T1omega.
Print E0.