Library Veq

Require Import Vbase.


Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Open Scope bool_scope.

Notation "x : T" := (x : T)
  (at level 100, right associativity,
   format "'[hv' x '/ ' : T ']'") : core_scope.

Notation "T : 'Type'" := (T%type : Type)
  (at level 100, only parsing) : core_scope.
Notation "P : 'Prop'" := (P%type : Prop)
  (at level 100, only parsing) : core_scope.

Delimit Scope eq_scope with EQ.
Open Scope eq_scope.


Section Contrapositives.

Variables (T : eqType) (b : bool) (x y : T).

Lemma contraTeq : (x != y -> negb b) -> b -> x = y.
Proof. by case b; case eqP; ins; exploit H. Qed.

Lemma contraNeq : (x != y -> b) -> negb b -> x = y.
Proof. by case b; case eqP; ins; exploit H. Qed.

Lemma contraTneq : (x = y -> negb b) -> b -> x != y.
Proof. by case b; case eqP; ins; exploit H. Qed.

Lemma contraNneq : (x = y -> b) -> negb b -> x != y.
Proof. by case b; case eqP; ins; exploit H. Qed.

End Contrapositives.

Theorem eq_irrelevance : forall (T : eqType) (x y : T) (e1 e2 : x = y), e1 = e2.
Proof.
intros; revert e2; subst y.
apply Eqdep_dec.K_dec; try done.
clear; intros; case (@eqP T x y); vauto.
Qed.

Corollary eq_axiomK : forall (T : eqType) (x : T), all_equal_to (Logic.eq_refl x).
Proof. by red; intros; apply @eq_irrelevance. Qed.

Module Type EqTypePredSig.
Parameter sort : eqType -> predArgType.
End EqTypePredSig.
Module MakeEqTypePred (eqmod : EqTypePredSig).
Coercion eqmod.sort : eqType >-> predArgType.
End MakeEqTypePred.
Module EqTypePred := MakeEqTypePred Equality.

Lemma unit_eqP : Equality.axiom (fun _ _ : unit => true).
Proof. intros [] []; vauto. Qed.

Definition unit_eqMixin := EqMixin unit_eqP.
Canonical Structure unit_eqType := Eval hnf in EqType unit unit_eqMixin.

Definition eqb (x y : bool) : bool :=
  match x, y with true, true => true | false, false => true | _, _ => false end.

Lemma eqbP : Equality.axiom eqb.
Proof. by intros [] []; constructor. Qed.

Canonical Structure bool_eqMixin := EqMixin eqbP.
Canonical Structure bool_eqType := Eval hnf in EqType bool bool_eqMixin.

Lemma eqbE : eqb = (@eq_op _).
Proof. done. Qed.

Lemma bool_irrelevance : forall (x y : bool) (E E' : x = y), E = E'.
Proof. apply eq_irrelevance. Qed.

Lemma negb_add : forall b1 b2, negb (xorb b1 b2) = (b1 == b2).
Proof. by intros [] []. Qed.

Lemma negb_eqb : forall b1 b2, (b1 != b2) = xorb b1 b2.
Proof. by intros [] []. Qed.

Lemma eqb_id : forall b, (b == true) = b.
Proof. by intros []. Qed.

Fixpoint eqn_rec (x y: nat) {struct x} :=
   match x, y with
     | O, O => true
     | S x, S y => eqn_rec x y
     | _, _ => false
   end.

Definition eqn := match tt with tt => eqn_rec end.

Lemma eqnP: forall x y, reflect (x = y) (eqn x y).
Proof.
  induction[] x [y]; vauto.
  change (eqn (S x) (S y)) with (eqn x y).
  case IHx; constructor; congruence.
Qed.

Canonical Structure nat_eqMixin := EqMixin eqnP.
Canonical Structure nat_eqType := Eval hnf in EqType nat nat_eqMixin.

Lemma eqnE : eqn = (@eq_op _).
Proof. done. Qed.

Lemma nat_irrelevance : forall (x y : nat) (E E' : x = y), E = E'.
Proof. apply eq_irrelevance. Qed.

Notation xpred1 := (fun a1 x => x == a1).
Notation xpred2 := (fun a1 a2 x => (x == a1) || (x == a2)).
Notation xpred3 := (fun a1 a2 a3 x => (x == a1) || (x == a2) || (x == a3)).
Notation xpred4 :=
   (fun a1 a2 a3 a4 x => (x == a1) || (x == a2) || (x == a3) || (x == a4)).
Notation xpredU1 := (fun a1 (p : pred _) x => (x == a1) || p x).
Notation xpredC1 := (fun a1 x => x != a1).
Notation xpredD1 := (fun (p : pred _) a1 x => (x != a1) && p x).

Section EqPred.

Variable T : eqType.

Definition pred1 (a1 : T) := SimplPred (xpred1 a1).
Definition pred2 (a1 a2 : T) := SimplPred (xpred2 a1 a2).
Definition pred3 (a1 a2 a3 : T) := SimplPred (xpred3 a1 a2 a3).
Definition pred4 (a1 a2 a3 a4 : T) := SimplPred (xpred4 a1 a2 a3 a4).
Definition predU1 (a1 : T) p := SimplPred (xpredU1 a1 p).
Definition predC1 (a1 : T) := SimplPred (xpredC1 a1).
Definition predD1 p (a1 : T) := SimplPred (xpredD1 p a1).

Lemma pred1E : pred1 =2 eq_op.
Proof. intros x y; simpl; apply beq_sym. Qed.

Variables (T2 : eqType) (x y : T) (z u : T2) (b : bool).

Lemma predU1P : reflect (x = y \/ b) ((x == y) || b).
Proof. eapply iffP; auto with vlib_refl; ins; desf; clarsimp; vauto. Qed.

Lemma pred2P : reflect (x = y \/ z = u) ((x == y) || (z == u)).
Proof. eapply iffP; auto with vlib_refl; ins; desf; clarsimp; vauto. Qed.

Lemma predD1P : reflect (x <> y /\ b) ((x != y) && b).
Proof. apply (iffP (andP _ _)); case eqP; ins; desf. Qed.

Lemma predU1l : x = y -> (x == y) || b.
Proof. by case eqP. Qed.

Lemma predU1r : b -> (x == y) || b.
Proof. by rewrite orbC; case b. Qed.

Lemma eqVneq : {x = y} + {x != y}.
Proof. by case eqP; [left | right]. Qed.

End EqPred.

Implicit Arguments predU1P [T x y b].
Implicit Arguments pred2P [T T2 x y z u].
Implicit Arguments predD1P [T x y b].

Notation "[ 'predU1' x & A ]" := (predU1 x [mem A])
  (at level 0, format "[ 'predU1' x & A ]") : fun_scope.
Notation "[ 'predD1' A & x ]" := (predD1 [mem A] x)
  (at level 0, format "[ 'predD1' A & x ]") : fun_scope.

Section EqFun.

Section Exo.

Variables (aT rT : eqType) (D : pred aT) (f : aT -> rT) (g : rT -> aT).

Lemma inj_eq : injective f -> forall x y, (f x == f y) = (x == y).
Proof.
intros inj_f x y; specialize (inj_f x y).
case eqP; case eqP; intuition congruence.
Qed.

Lemma can_eq : cancel f g -> forall x y, (f x == f y) = (x == y).
Proof. eby intros; eapply inj_eq, can_inj. Qed.

Lemma bij_eq : bijective f -> forall x y, (f x == f y) = (x == y).
Proof. by intros; apply inj_eq, bij_inj. Qed.

Lemma can2_eq : cancel f g -> cancel g f -> forall x y, (f x == y) = (x == g y).
Proof. by intros; rewrite <- (H0 y) at 1; apply can_eq. Qed.

Lemma inj_in_eq :
  {in D &, injective f} -> {in D &, forall x y, (f x == f y) = (x == y)}.
Proof. by intros inj_f x y Dx Dy; do 2 case eqP; clarsimp; apply inj_f in e. Qed.

Lemma can_in_eq :
  {in D, cancel f g} -> {in D &, forall x y, (f x == f y) = (x == y)}.
Proof. eauto using inj_in_eq, can_in_inj. Qed.

End Exo.

Section Endo.

Variables (T : eqType) (f : T -> T).

Definition frel := [rel x y : T | f x == y].

Lemma inv_eq : involutive f -> forall x y, (f x == y) = (x == f y).
Proof. by intros; apply can2_eq. Qed.

End Endo.

Variable aT : Type.


Definition invariant (rT : eqType) f (k : aT -> rT) :=
  [pred x | k (f x) == k x].

Variables (rT1 rT2 : eqType) (f : aT -> aT) (h : rT1 -> rT2) (k : aT -> rT1).

Lemma invariant_comp : subpred (invariant f k) (invariant f (h \o k)).
Proof. by red; ins; rewrite (eqP _ _ H). Qed.

Lemma invariant_inj : injective h -> invariant f (h \o k) =1 invariant f k.
Proof. by red; ins; apply inj_eq. Qed.

End EqFun.


Section FunWith.

Variables (aT : eqType) (rT : Type).

Inductive fun_delta : Type := FunDelta (_ : aT) (_ : rT).

Definition fwith x y (f : aT -> rT) := [fun z => if z == x then y else f z].

Definition app_fdelta df f z :=
  match df with FunDelta x y => if z == x then y else f z end.

End FunWith.


Notation "x |-> y" := (FunDelta x y)
  (at level 190, no associativity,
   format "'[hv' x '/ ' |-> y ']'") : fun_delta_scope.

Delimit Scope fun_delta_scope with FUN_DELTA.
Arguments Scope app_fdelta [_ type_scope fun_delta_scope _ _].

Definition SimplFunDelta aT rT (f : aT -> aT -> rT) := [fun z => f z z].

Notation "[ 'fun' z : T => F 'with' d1 , .. , dn ]" :=
  (SimplFunDelta (fun z : T =>
     app_fdelta d1%FUN_DELTA .. (app_fdelta dn%FUN_DELTA (fun _ => F)) ..))
  (at level 0, z ident, only parsing) : fun_scope.

Notation "[ 'fun' z => F 'with' d1 , .. , dn ]" :=
  (SimplFunDelta (fun z =>
     app_fdelta d1%FUN_DELTA .. (app_fdelta dn%FUN_DELTA (fun _ => F)) ..))
  (at level 0, z ident, format
   "'[hv' [ '[' 'fun' z => '/ ' F ']' '/' 'with' '[' d1 , '/' .. , '/' dn ']' ] ']'"
   ) : fun_scope.

Notation "[ 'eta' f 'with' d1 , .. , dn ]" :=
  (SimplFunDelta (fun _ =>
     app_fdelta d1%FUN_DELTA .. (app_fdelta dn%FUN_DELTA f) ..))
  (at level 0, z ident, format
  "'[hv' [ '[' 'eta' '/ ' f ']' '/' 'with' '[' d1 , '/' .. , '/' dn ']' ] ']'"
  ) : fun_scope.

Section ComparableType.

Variable T : Type.

Definition comparable := forall x y : T, {x = y} + {x <> y}.

Hypothesis Hcompare : forall x y : T, {x = y} + {x <> y}.

Definition compareb x y :=
  match Hcompare x y with
    | left _ => true
    | right _ => false
  end.

Lemma compareP : Equality.axiom compareb.
Proof. by intros x y; unfold compareb; case (Hcompare x y); constructor. Qed.

Definition comparableClass := EqMixin compareP.

End ComparableType.

Definition eq_comparable (T : eqType) : comparable T :=
  fun x y => decP (eqP x y).

Section SubType.

Variables (T : Type) (P : pred T).

Structure subType : Type := SubType {
  sub_sort :> Type;
  val : sub_sort -> T;
  Sub : forall x, P x -> sub_sort;
  _ : forall K (_ : forall x Px, K (@Sub x Px)) u, K u;
  _ : forall x Px, val (@Sub x Px) = x
}.

Implicit Arguments Sub [s].
Lemma vrefl : forall x, P x -> x = x.
Proof. done. Qed.

Definition clone_subType U v :=
  fun sT (_ : sub_sort sT -> U) =>
  fun c Urec cK (sT' := @SubType U v c Urec cK) (_ : phant_id sT' sT) => sT'.

Variable sT : subType.

Inductive Sub_spec : sT -> Type := SubSpec x Px : Sub_spec (Sub x Px).

Lemma SubP : forall u, Sub_spec u.
Proof. by generalize Sub_spec SubSpec; case sT. Qed.

Lemma SubK : forall x Px, @val sT (Sub x Px) = x.
Proof. by case sT. Qed.

Definition insub x :=
  match @idP (P x) with
    | ReflectT Px => @Some sT (Sub x Px)
    | ReflectF _ => None
  end.

Definition insubd u0 x := odflt u0 (insub x).

Inductive insub_spec x : option sT -> Type :=
  | InsubSome: forall u (_: P x) (_ : val u = x), insub_spec x (Some u)
  | InsubNone: forall (_: negb (P x)), insub_spec x None.

Lemma insubP : forall x, insub_spec x (insub x).
Proof.
unfold insub; intros; generalize (@idP (P x)); generalize (P x) at 2.
by destruct r as [X|X]; [left; rewrite ?SubK | right; apply/negP].
Qed.

Lemma insubT : forall x Px, insub x = Some (Sub x Px).
Proof.
intros x; case insubP; [|by case negP].
intro u; destruct (SubP u); intros.
by rewrite SubK in *; clarify; rewrite (bool_irrelevance Px Px0).
Qed.

Lemma insubF : forall x, P x = false -> insub x = None.
Proof. intros; case insubP; clarsimp. Qed.

Lemma insubN : forall x, negb (P x) -> insub x = None.
Proof. by intros; apply insubF; destruct (P x). Qed.
Lemma insubK : ocancel insub (@val _).
Proof. by intro; case insubP. Qed.

Lemma valP : forall u : sT, P (val u).
Proof. by intros; destruct (SubP u); rewrite SubK. Qed.

Lemma valK : pcancel (@val _) insub.
Proof. intro u; case (SubP u); intros x Px; rewrite SubK; apply insubT. Qed.

Lemma val_inj : injective (@val sT).
Proof. apply (pcan_inj valK). Qed.

Lemma valKd : forall u0, cancel (@val _) (insubd u0).
Proof. by intros u0 u; unfold insubd; rewrite valK. Qed.

Lemma val_insubd : forall u0 x, val (insubd u0 x) = if P x then x else val u0.
Proof.
by unfold insubd; intros u0 x; case insubP; clarsimp; rewrite (negPf i).
Qed.

Lemma insubdK : forall u0, {in P, cancel (insubd u0) (@val _)}.
Proof. by intros u0 x Px; rewrite val_insubd, Px. Qed.

Definition insub_eq x :=
  let Some_sub Px := Some (Sub x Px : sT) in
  let None_sub _ := None in
  (if P x as Px return P x = Px -> _ then Some_sub else None_sub) Logic.eq_refl.

Lemma insub_eqE : insub_eq =1 insub.
Proof.
unfold insub_eq, insub; intros x.
generalize (Logic.eq_refl (P x)), (@idP (P x)); generalize (P x) at 2 4 5.
by destruct r; clarify; repeat f_equal; apply eq_irrelevance.
Qed.

End SubType.

Implicit Arguments SubType [T P].
Implicit Arguments Sub [T P s].
Implicit Arguments vrefl [T P].
Implicit Arguments clone_subType [T P sT c Urec cK].
Implicit Arguments insub [T P sT].
Implicit Arguments insubT [T sT x].
Implicit Arguments val_inj [T P sT].
Implicit Arguments val [[T] [P] [s]].

Notation "[ 'subType' 'for' v 'by' rec ]" := (SubType _ v _ rec vrefl)
 (at level 0, format "[ 'subType' 'for' v 'by' rec ]") : form_scope.

Notation "[ 'subType' 'for' v , U ]" := (clone_subType U v id [eta idfun])
 (at level 0, format "[ 'subType' 'for' v , U ]") : form_scope.

Notation "[ 'subType' 'for' v ]" := (clone_subType _ v id idfun)
 (at level 0, format "[ 'subType' 'for' v ]") : form_scope.

Notation "[ 'subType' 'of' U ]" := (clone_subType U _ id id)
 (at level 0, format "[ 'subType' 'of' U ]") : form_scope.

Definition NewType T U v c Urec :=
  let Urec' P IH := Urec P (fun x : T => IH x (eq_refl true) : P _) in
  SubType U v (fun x _ => c x) Urec'.
Implicit Arguments NewType [T U].

Notation "[ 'newType' 'for' v 'by' rec ]" := (NewType v _ rec vrefl)
 (at level 0, format "[ 'newType' 'for' v 'by' rec ]") : form_scope.

Definition innew T nT x := @Sub T predT nT x (eq_refl true).
Implicit Arguments innew [[T] [nT]].

Lemma innew_val : forall T nT, cancel val (@innew T nT).
Proof. by intros T nT u; apply val_inj, SubK. Qed.

Notation sval := (@proj1_sig _ _).
Notation "@ 'sval'" := (@proj1_sig) (at level 10, format "@ 'sval'").

Section SigProj.

Variables (T : Type) (P Q : T -> Prop).

Lemma svalP : forall u : sig P, P (sval u).
Proof. by intros []. Qed.

Definition s2val (u : sig2 P Q) := match u with exist2 x _ _ => x end.

Lemma s2valP : forall u, P (s2val u).
Proof. by intros []. Qed.

Lemma s2valP' : forall u, Q (s2val u).
Proof. by intros []. Qed.

End SigProj.


Section TransferEqType.

Variables (T : Type) (eT : eqType) (f : T -> eT).

Lemma inj_eqAxiom : injective f -> Equality.axiom (fun x y => f x == f y).
Proof. intros f_inj x y. apply (iffP (eqP _ _)); autos. Qed.

Definition InjEqMixin f_inj := EqMixin (inj_eqAxiom f_inj).

Definition PcanEqMixin g (fK : pcancel f g) := InjEqMixin (pcan_inj fK).

Definition CanEqMixin g (fK : cancel f g) := InjEqMixin (can_inj fK).

End TransferEqType.

Section SubEqType.

Variables (T : eqType) (P : pred T) (sT : subType P).

Notation Local ev_ax := (fun T v => @Equality.axiom T (fun x y => v x == v y)).

Lemma val_eqP : ev_ax sT val.
Proof. by simpl; apply inj_eqAxiom, val_inj. Qed.

Definition sub_eqMixin := EqMixin val_eqP.
Canonical Structure sub_eqType := Eval hnf in EqType sT sub_eqMixin.

Definition SubEqMixin :=
  (match sT as sT' return ev_ax sT' val -> Equality.class_of sT' with
     | SubType _ v _ _ _ =>
   fun vP : ev_ax _ v => EqMixin vP
   end) val_eqP.

Lemma val_eqE : forall u v : sT, (val u == val v) = (u == v).
Proof. done. Qed.

End SubEqType.

Implicit Arguments val_eqP [[T] [P] [sT] x y].

Notation "[ 'eqMixin' 'of' T 'by' <: ]" := (SubEqMixin _ : Equality.class_of T)
  (at level 0, format "[ 'eqMixin' 'of' T 'by' <: ]") : form_scope.

Section SigEqType.

Variables (T : eqType) (P : pred T).

End SigEqType.

Section ProdEqType.

Variable T1 T2 : eqType.

Definition pair_eq := [rel u v : T1 * T2 | (fst u == fst v) && (snd u == snd v)].

Lemma pair_eqP : Equality.axiom pair_eq.
Proof.
intros [x1 x2] [y1 y2]; simpl; apply (iffP (andP _ _)); clarsimp; desf; clarify.
Qed.

Definition prod_eqMixin := EqMixin pair_eqP.
Canonical Structure prod_eqType := Eval hnf in EqType (T1 * T2) prod_eqMixin.

Lemma pair_eqE : pair_eq = eq_op :> rel _.
Proof. done. Qed.

Lemma xpair_eqE : forall (x1 y1 : T1) (x2 y2 : T2),
  ((x1, x2) == (y1, y2)) = ((x1 == y1) && (x2 == y2)).
Proof. done. Qed.

Tactic Notation "move" "/" reference(X) hyp_list(Y) :=
  revert Y; let top := fresh in intro top;
  first [ generalize (X top); clear top
        | generalize (X _ top); clear top
        | generalize (X _ _ top); clear top
        | generalize (X _ _ _ top); clear top
        | generalize (X _ _ _ _ top); clear top
        | apply X in top; revert top
        | apply -> X in top; revert top
        | apply <- X in top; revert top].

Variables u v : T1 * T2.

Lemma pair_eq1 : u == v -> fst u == fst v.
Proof. case u, v; move/andP; tauto. Qed.

Lemma pair_eq2 : u == v -> snd u == snd v.
Proof. case u, v; move/andP; tauto. Qed.

End ProdEqType.

Definition predX T1 T2 (p1 : pred T1) (p2 : pred T2) :=
  [pred z | p1 (fst z) && p2 (snd z)].

Notation "[ 'predX' A1 & A2 ]" := (predX [mem A1] [mem A2])
  (at level 0, format "[ 'predX' A1 & A2 ]") : fun_scope.

Section OptionEqType.

Variable T : eqType.

Definition opt_eq (u v : option T) : bool :=
  oapp (fun x => oapp (eq_op x) false v) (match v with Some _ => false | None => true end) u.

Lemma opt_eqP : Equality.axiom opt_eq.
Proof.
red; intros [x|] [y|]; simpls; vauto.
apply (iffP (@eqP _ _ _)); clarsimp.
Qed.

Canonical Structure option_eqMixin := EqMixin opt_eqP.
Canonical Structure option_eqType :=
  Eval hnf in EqType (option T) option_eqMixin.

End OptionEqType.

Definition tag := projS1.
Definition tagged I T_ : forall u, T_(tag u) := @projS2 I [eta T_].
Definition Tagged I i T_ x := @existS I [eta T_] i x.
Implicit Arguments Tagged [I i].

Section TaggedAs.

Variables (I : eqType) (T_ : I -> Type).
Implicit Types u v : {i : I & T_ i}.

Definition tagged_as u v :=
  match eqP (tag u) (tag v) with
    | ReflectT eq_uv => eq_rect_r T_ (tagged v) eq_uv
    | _ => tagged u
  end.

Lemma tagged_asE : forall u x, tagged_as u (Tagged T_ x) = x.
Proof.
  ins; unfold tagged_as; case eqP; simpls.
  by intros; rewrite eq_axiomK.
Qed.

End TaggedAs.

Section TagEqType.

Variables (I : eqType) (T_ : I -> eqType).
Implicit Types u v : {i : I & T_ i}.

Definition tag_eq u v := (tag u == tag v) && (tagged u == tagged_as u v).

Lemma tag_eqP : Equality.axiom tag_eq.
Proof.
  red; destruct x, y; unfold tag_eq; ins.
  case eqP; simpls; [|constructor]; intro; clarify.
  assert (M:= tagged_asE); unfold Tagged in M.
  by apply (iffP (eqP _ _)); [intros ->|intros <-]; rewrite M.
Qed.

Canonical Structure tag_eqMixin := EqMixin tag_eqP.
Canonical Structure tag_eqType := Eval hnf in EqType {i : I & T_ i} tag_eqMixin.

Lemma tag_eqE : tag_eq = eq_op.
Proof. done. Qed.

Lemma eq_tag u v : u == v -> tag u = tag v.
Proof. by move/eqP; intro; clarify. Qed.

Lemma eq_Tagged u x : (u == Tagged _ x) = (tagged u == x).
Proof. by rewrite <-tag_eqE; unfold tag_eq; rewrite eqxx, tagged_asE. Qed.

End TagEqType.

Implicit Arguments tag_eqP [I T_ x y].

Section SumEqType.

Variables T1 T2 : eqType.
Implicit Types u v : T1 + T2.

Definition sum_eq u v :=
  match u, v with
  | inl x, inl y | inr x, inr y => x == y
  | _, _ => false
  end.

Lemma sum_eqP : Equality.axiom sum_eq.
Proof. case x, y; simpl; vauto; case eqP; constructor; congruence. Qed.

Canonical Structure sum_eqMixin := EqMixin sum_eqP.
Canonical Structure sum_eqType := Eval hnf in EqType (T1 + T2) sum_eqMixin.

Lemma sum_eqE : sum_eq = eq_op.
Proof. done. Qed.

End SumEqType.

Implicit Arguments sum_eqP [T1 T2 x y].