Require Import Arith.

(* reification using canonical structures, directly inspired from models
  given in ssreflect, for instance in a tactic to compute the rank of
  a "direct sum of matrices". *)

Module first_example.

Parameters (A : Type) (op : A -> A -> A).
Local Infix "+" := op.

Inductive bin : Type := L (x : A) | N (t1 t2 : bin).

Fixpoint f (t : bin) := match t with L x => x | N t1 t2 => f t1 + f t2 end.

Structure map := Map {pn; pt : bin; pf : f pt = pn}.

Fact binmap_proof : forall m1 m2, f (N (pt m1) (pt m2)) = pn m1 + pn m2.
intros [n1 t1 f1][n2 t2 f2]; simpl; rewrite f1, f2; reflexivity.
Qed.

Canonical Structure binmap (m1 m2 : map) :=
  Map (pn m1 + pn m2) (N (pt m1) (pt m2)) (binmap_proof m1 m2).

Canonical Structure leafmap (x : A) := Map x (L x) (refl_equal _).

Lemma trig : forall m1 m2, f (pt m1) = f (pt m2) -> pn m1 = pn m2.
intros [n1 t1 prf1] [n2 t2 prf2]; simpl; rewrite prf1, prf2; trivial.
Qed.

Infix "+" := N : bscope.
Delimit Scope bscope with bin.

Section example_without_definitions.
(* A function that works on reified values, with the assumption that it
  preserves equalities of values as computed by f. If this was the example
  in Coq'Art sect. 16.3.1, g and g_eq would be flatten flatten_valid_2.  *)
Variable g : bin -> bin.
Hypothesis g_eq : forall t1 t2, f (g t1) = f (g t2) -> f t1 = f t2.
Lemma example : 
  forall x y z t u,
      (g (L x + L y + L z + L t + L u) =
       g (L x + (L y + (L z + (L t + L u)))))%bin ->
      x + y + z + t + u = x + (y + (z + (t + u))).
(* The reification step *)
intros x y z t u q.
refine (trig _ _ _).
simpl pt.
(* The reflexion step. *)
apply g_eq; rewrite q; reflexivity.
Qed.
End example_without_definitions.

End first_example.