Require Import List Reals ZArith.
From HB Require Import structures.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

(* experiments learning HB, first round *)


(* first experiment: a naive structure with a set endowed with an involution, with
   some trivial instances and a stupid theorem *)

HB.mixin Record Involutive_Type M := {
  inv: M -> M;
  self_inv: forall m, inv (inv m) = m;
}.

HB.structure Definition Involutive := { M of Involutive_Type M }.

HB.instance Definition Z_involutive := Involutive_Type.Build Z Z.opp_involutive.
HB.instance Definition R_involutive := Involutive_Type.Build R Ropp_involutive.

Lemma thrice_once (M: Involutive.type): forall (m: M), inv (inv (inv m)) = inv m.
Proof.
intro m.
apply self_inv.
Qed.

(* second experiment: a set with a reflexive&transitive relation, trivial instances and
   a less trivial one *)

HB.mixin Record is_CmpSet M := {
  cmp: M -> M -> Prop;
  cmp_reflexive: forall m, cmp m m;
  cmp_transitive: forall m n p, cmp m n -> cmp n p -> cmp m p;
}.

HB.structure Definition CmpSet := { M of is_CmpSet M}.

HB.instance Definition nat_cmp := is_CmpSet.Build nat le_refl le_trans.
HB.instance Definition N_cmp := is_CmpSet.Build N N.le_refl N.le_trans.
HB.instance Definition Z_cmp := is_CmpSet.Build Z Z.le_refl Z.le_trans.

Fixpoint cmp_list {A} (l1 l2: list A) := (* it's just a length comparison *)
  match l1 with
  | nil => True
  | h1 :: t1 => match l2 with | nil => False | h2 :: t2 => cmp_list t1 t2 end
  end.

Lemma cmp_list_reflexive {A}: forall (l: list A), cmp_list l l.
Proof.
intro l.
induction l.
  unfold cmp_list.
  auto.
unfold cmp_list.
auto.
Qed.

Lemma cmp_list_transitive {A}: forall (l1 l2 l3: list A), cmp_list l1 l2 -> cmp_list l2 l3 -> cmp_list l1 l3.
Proof.
intros l1.
induction l1.
  auto.
induction l2.
  unfold cmp_list at 1 2.
  intro l3.
  apply (False_ind (True -> cmp_list (a::l1) l3)). (* FIXME: why so complex? *)
induction l3.
  simpl.
  auto.
simpl.
apply IHl1.
Qed.

HB.instance Definition list_cmp {A} := is_CmpSet.Build (list A) cmp_list_reflexive cmp_list_transitive.


(* third experiment: push the previous one further, trying to play the "structure transfert" game
   with a pullback trick *)

Section Pullback.

Variable Source: Type.
Variable Destination: CmpSet.type.
Variable f: Source -> Destination.

Definition cmp_pullback (s1 s2: Source) := cmp (f s1) (f s2).

Lemma cmp_pullback_reflexive: forall s, cmp_pullback s s.
Proof.
intro s.
unfold cmp_pullback.
apply cmp_reflexive.
Qed.

Lemma cmp_pullback_transitive: forall s1 s2 s3, cmp_pullback s1 s2 -> cmp_pullback s2 s3 -> cmp_pullback s1 s3.
Proof.
intros s1 s2 s3.
unfold cmp_pullback.
apply cmp_transitive.
Qed.

HB.instance Definition pullback_cmp :=
   is_CmpSet.Build Source cmp_pullback_reflexive cmp_pullback_transitive.

End Pullback.

Check (pullback_cmp (@length _)).

(* fourth experiment: can I express that pulling back `length` from the
   integers to the lists will give me the same comparison? and then:
   can I prove it? *)

(* FIXME:
 1. I'd like to write it with `cmp` pointing out which structure I want, not by using
    explicit `cmp_list` and `cmp_pullback`
 2. Using `(@length A)` instead of just `length` seems a bit awkward ; indeed length seems generic,
    but since I declared the list types, the fact that it's *this* length seems pretty explicit!
 3. The proof I wrote is pretty long... the fact I wanted to use bare Coq and not SSR might not have
    helped, but I wonder if I didn't miss something nice.
  *)
Lemma coherent_cmp_on_list (A: Type) (l1 l2: list A):
      iff (cmp_pullback (@length A) l1 l2) (cmp_list l1 l2).
Proof.
split.
(* first implication *)
revert l2.
induction l1.
  simpl.
  auto.
induction l2.
  unfold cmp_pullback.
  unfold cmp.
  simpl.
  apply Nat.nle_succ_0.
unfold cmp_pullback.
unfold cmp.
simpl.
intro lel1l2.
apply le_S_n in lel1l2.
apply IHl1.
unfold cmp_pullback.
unfold cmp.
auto.

(* second implication *)
revert l2.
induction l1.
  unfold cmp_pullback.
  unfold cmp.
  simpl.
  intros l2 T.
  apply Nat.le_0_l.
induction l2.
  unfold cmp_pullback.
  unfold cmp.
  simpl.
  apply False_ind.
unfold cmp_pullback.
unfold cmp.
simpl.
intro cmpl1l2.
apply le_n_S.
apply IHl1.
exact cmpl1l2.
Qed.