Mtac2 Port of a reification/reflection example from elpi.

elpi-reification-port.v

(*
  Installing Mtac2 for 8.11:

  opam repo add mtac2-dev git+https://github.com/Mtac2/opam.git
  opam update mtac2-dev
  opam install coq-mtac2.dev.8.11

 *)


(* Monoid theory from:
https://github.com/LPCIC/coq-elpi/blob/dcdf72a01884751a4fe4e2a82a8a2ae77b7d5b23/theories/examples/example_reflexive_tactic.v
 *)

Require Arith ZArith Psatz List ssreflect.

Import Arith ZArith Psatz List ssreflect.

(* This module contains the reflexive normalizer and its correctness proof *)
Module MonoidTheory.

(* The syntax of terms *)
Inductive lang :=
| var (i : nat)        (* i-th variable in the context *)
| zero : lang          (* Neutral element *)
| add (x y : lang).    (* binary operation *)

(* Interpretation to T *)
Fixpoint interp T (e : T) (op : T -> T -> T) (gamma : list T) (t : lang) : T :=
  match t with
  | var v => nth v gamma e
  | zero => e
  | add x y => op (interp T e op gamma x) (interp T e op gamma y)
  end.
 

 (* normalization of parentheses and units *)
 Fixpoint normAx t1 acc :=
   match t1 with
   | add t1 t2 => normAx t1 (normAx t2 acc)
   | _ => add t1 acc
   end.
 Fixpoint normA t :=
   match t with
   | add s1 s2 => normAx s1 (normA s2)
   | _ => t
   end.
 Fixpoint norm1 t :=
  match t with
  | var _ => t
  | zero => t
  | add t1 t2 =>
     match norm1 t1 with
     | zero => norm1 t2
     | t1 =>
         match norm1 t2 with
         | zero => t1
         | t2 => add t1 t2
         end
     end
  end.
 Definition norm t := normA (norm1 t).

  (* Correctness theorem. This is not the point of this demo, please don't
     look at the proofs ;-) *)
 Section assoc_reflection_proofs.
 Variable T : Type.
 Variable unit : T.
 Variable op : T -> T -> T.
 Hypothesis op_assoc : forall a b c, op a (op b c) = op (op a b) c.
 Hypothesis unit_l : forall a, op unit a = a.
 Hypothesis unit_r : forall a, op a unit = a.

Lemma normAxA t1 t2 : normAx t1 (normA t2) = normA (add t1 t2).
Proof. by []. Qed.

Lemma normAx_add {t1 t2 s} : normAx t1 t2 = s -> exists s1 s2, s = add s1 s2.
Proof.
elim: t1 t2 s => /= [i||w1 H1 w2 H2] t2 s <-; try by do 2 eexists; reflexivity.
by case E: (normAx _ _); case/H1: E => s1 [s2 ->]; do 2 eexists; reflexivity.
Qed.

Lemma norm1_zero {l t} : norm1 t = zero -> interp T unit op l t = unit.
Proof.
by elim: t => [||s1 + s2] //=; case E1: (norm1 s1); case E2: (norm1 s2) => //= -> // ->.
Qed.

Lemma norm_zero {l t} : norm t = zero -> interp T unit op l t = unit.
Proof.
rewrite /norm; case E: (norm1 t) => [||x y] //; first by rewrite (norm1_zero E).
by move/normAx_add=> [] ? [].
Qed.

Lemma norm1_var {l t j} : norm1 t = var j -> interp T unit op l t = nth j l unit.
Proof.
elim: t => [i [->]||s1 + s2] //=; case E1: (norm1 s1); case E2: (norm1 s2) => //=.
  by rewrite (norm1_zero E2) unit_r => + _ H => ->.
by rewrite (norm1_zero E1) unit_l => _ + H => ->.
Qed.

Lemma norm_var {l t j} : norm t = var j -> interp T unit op l t = nth j l unit.
Proof.
rewrite /norm; case E: (norm1 t); rewrite /= ?(norm1_var E) //; first by move=> [->].
by move/normAx_add=> [] ? [].
Qed.

Lemma norm1_add {l t s1 s2} : norm1 t = add s1 s2 -> interp T unit op l t = op (interp T unit op l s1) (interp T unit op l s2).
Proof.
elim: t s1 s2 => [||w1 + w2 + s1 s2] //=.
by case E1: (norm1 w1); case E2: (norm1 w2) => //= ++ [<- <-] /=;
  do 2! [ move=> /(_ _ _ (refl_equal _)) -> | move=> _];
  rewrite ?(norm1_zero E1) ?(norm1_zero E2) ?(norm1_var E1) ?(norm1_var E2).
Qed.

Lemma normAxP {l t1 t2} : interp T unit op l (normAx t1 t2) = op (interp T unit op l t1) (interp T unit op l t2).
Proof. by elim: t1 t2 => [||s1 Hs1 s2 Hs2] t2 //=; rewrite Hs1 Hs2 !op_assoc. Qed.

Lemma normAP {l} t : interp T unit op l (normA t) = interp T unit op l t.
Proof. by elim: t => //= x Hx y Hy; rewrite normAxP Hy. Qed.

Lemma norm_add {l t s1 s2} : norm t = add s1 s2 -> interp T unit op l t = op (interp T unit op l s1) (interp T unit op l s2).
Proof.
rewrite /norm; case E: (norm1 t) => [||x y]; rewrite //= (norm1_add E).
elim: x y s1 s2 {E} => //= [>[<- <- //=]|>[<- <-]|x + y + w s1 s2]; rewrite ?normAP //= ?unit_l //.
by rewrite normAxA -!op_assoc => ++ E => /(_ _ _ _ E) ->.
Qed.

Lemma normP_ l t1 t2 : norm t1 = norm t2 -> interp T unit op l t1 = interp T unit op l t2.
Proof.
case E: (norm t2) => [?||??] => [/norm_var|/norm_zero|/norm_add] ->.
  by rewrite (norm_var E).
  by rewrite (norm_zero E).
by rewrite (norm_add E).
Qed.

End assoc_reflection_proofs.
End MonoidTheory.

Import MonoidTheory.

(* This is the correctness theorem of our normalizer *)
Definition normP {T e op gamma t1 t2} p1 p2 p3 H := @normP_ T e op p1 p2 p3 gamma t1 t2 H.
About normP.


Open Scope Z_scope.

Goal forall x y z t, (x + y) + (z + 0 + t) = x + (y + z) + t.
Proof.
intros.

change (interp Z Z.zero Z.add (x::y::z::t::nil)
             (add (add (var 0) (var 1)) (add (add (var 2) zero) (var 3)))
        =
        interp Z Z.zero Z.add (x::y::z::t::nil)
              (add (add (var 0) (add (var 1) (var 2))) (var 3))).

apply: normP Z.add_assoc Z.add_0_l Z.add_0_r _.

reflexivity.
Qed.


(** Canonical structures to find monoids on types (to be used later). *)
Structure Monoid :=
  {
    monoid_type :> Type;
    monoid_zero : monoid_type;
    monoid_add : monoid_type -> monoid_type -> monoid_type
  }.
Arguments monoid_zero {_}.
Arguments monoid_add {_} _ _.

Canonical Z_Monoid : Monoid := Build_Monoid Z 0 Z.add.


(** Mtac2 port of the reification tactic *)

From Mtac2 Require Import Mtac2 Tactics Ttactics.

(** Ltac-style tactics *)

(** V1 is a very imperative version using dynamically-typed, i.e. Ltac-style tactics *)
Module Mtac_V1.

  Definition VarNotFound : Exception. constructor. Qed.
  (* Helper to find the position of a variable in a list.
     [L] is reversed so the position is the length of the suffix. *)
  Definition pos_of {T} (var : T) :=
    let go := mfix1 go (L : list T) : M nat :=
      mmatch L return M _ with
      | [? L'] var :: L' =>
        let pos := reduce RedVmCompute (List.length L') in M.ret pos
      | [? x L'] x :: L' => go L'
      | nil => M.raise VarNotFound
      end
    in go.

  (* [gtactic] is a tactic that also returns a value.
     The inner fixpoint will return the list of variables in reverse order to avoid stacking list appends.
   *)
  Definition reify {T} (op_zero : T) (op_add : T -> T -> T) (t : T) : gtactic (list T * lang) :=
    let go :=
        mfix2 go (L : list T) (t : T) : gtactic (list T * lang) :=
          mmatch t return gtactic _ with
          | op_zero => T.ret (L, zero)
          | [? x y] op_add x y =>
            '(L, x) <- go L x;
            '(L, y) <- go L y;
            T.ret (L, add x y)
          | _ =>
            mtry
              pos <- pos_of t L;
              T.ret (L, var pos)
            with VarNotFound =>
              (* We could track [n] as an argument to [go] if this computation ever becomes a bottleneck *)
              let pos := reduce (RedVmCompute) (List.length L) in
              T.ret (t :: L, var pos)
            end
          | _ => fun _ => mfail "Encountered unknown term: " t
        end
    in
    '(L_rev, t') <- go nil t;
    let L := reduce (RedVmCompute) (rev L_rev) in
    T.ret (L, t')
  .


  Definition monoid {T} (op_zero : T) (op_add : T -> T -> T) : tactic :=
    match_goal with
    | [[? (x y : T) |- x = y ]] =>
      '(Lx, x) <- reify op_zero op_add x;
      '(Ly, y) <- reify op_zero op_add y;
      T.change (interp T op_zero op_add Lx x = interp T op_zero op_add Ly y)
    | [[? g : Prop |- g ]] => fun _ => mfail "Encountered unknown goal: " g
    end.

  Goal forall x y z t, (x + y) + (z + 0 + t) = x + (y + z) + t.
  Proof.
    intros.
    mrun (monoid 0 Z.add).
    apply: normP Z.add_assoc Z.add_0_l Z.add_0_r _.
    reflexivity.
  Qed.

  (* Let's use canonical structures to look up monoid operators *)
  Definition monoid_lookup : tactic :=
    match_goal with
    | [[? (M : Monoid) (x y : M) |- x = y ]] =>
      '(Lx, x) <- reify monoid_zero monoid_add x;
      '(Ly, y) <- reify monoid_zero monoid_add y;
      T.change (interp M monoid_zero monoid_add Lx x = interp M monoid_zero monoid_add Ly y)
    | [[? g : Prop |- g ]] => fun _ => mfail "Encountered unknown goal: " g
    end.

  Canonical Z_Monoid : Monoid := Build_Monoid Z 0 Z.add.

  Goal forall x y z t, (x + y) + (z + 0 + t) = x + (y + z) + t.
  Proof.
    intros.
    mrun (monoid_lookup).       (* no more arguments *)
    apply: normP Z.add_assoc Z.add_0_l Z.add_0_r _.
    reflexivity.
  Qed.

End Mtac_V1.


(* V2 uses a unification variable to build the list of variables (mirroring the elpi solution). *)
Module Mtac_V2.

  (* Helper to find the position of a variable in a list.

     New in V2:
     - No case for [nil] since [L] ends in an evar.
     - The [var :: L' =u> ..] pattern will extend the list if [var] cannot be found in [L] proper.
   *)
  Definition pos_of {T} (var : T) :=
    let go := mfix2 go (pos : nat) (L : list T) : M nat :=
      mmatch L return M _ with
      | [? L'] var :: L' =u> M.ret pos
      | [? x L'] x :: L' => go (S pos) L'
      (* we no longer need a pattern for the empty list since we'll always find our variable in the tail evar. *)
      (* | _ => mfail "Impossible case: " L *)
      end%MC
    in go (0%nat).


    (* Instantiate evar tail with [nil] *)
    Definition end_list {T} := (mfix1 end_list (L : list T) : M unit :=
       mmatch L with
      | [? x L] x :: L =n> end_list L
      | _ => _ <- M.unify_or_fail UniCoq L nil; M.ret tt
     end)%MC.

  (* [gtactic] is a tactic that also returns a value.
     Unlike in V1, we do not explicitly return [L] from the inner [mfix] since we use side effects (unification) to construct it.
     The resulting [L] is also not reversed.
   *)
  Definition reify {T} (op_zero : T) (op_add : T -> T -> T) (t : T) : gtactic (list T * lang) :=
    (* let fixup_evars (go : list T -> list T -> t -> gtactic (list T * lang) :=  *)
    (* the invariant of [go] is that [L] ends in [tail] *)
    let go :=
        mfix2 go (L: list T) (t : T) : gtactic (lang) :=
          mmatch t return gtactic _ with
          | op_zero => T.ret (zero)
          | [? x y] op_add x y =>
            x <- go L x;
            y <- go L y;
            T.ret (add x y)
          | _ =>
            pos <- pos_of t L;
            T.ret (var pos)
          | _ => fun _ => mfail "Encountered unknown term: " t
        end
    in
    `L <- M.evar _;
    t' <- go L t;
    end_list L;;
    T.ret (L, t')
  .

  Definition monoid {T} (op_zero : T) (op_add : T -> T -> T) : tactic :=
    match_goal with
    | [[? (x y : T) |- x = y ]] =>
      '(Lx, x) <- reify op_zero op_add x;
      '(Ly, y) <- reify op_zero op_add y;
      T.change (interp T op_zero op_add Lx x = interp T op_zero op_add Ly y)
    | [[? g : Prop |- g ]] => fun _ => mfail "Encountered unknown goal: " g
    end.

  Goal forall x y z t, (x + y) + (z + 0 + t) = x + (y + z) + t.
  Proof.
    intros.
    mrun (monoid 0 Z.add).
    apply: normP Z.add_assoc Z.add_0_l Z.add_0_r _.
    reflexivity.
  Qed.

  Definition monoid_lookup : tactic :=
    match_goal with
    | [[? (M : Monoid) (x y : M) |- x = y ]] =>
      '(Lx, x) <- reify monoid_zero monoid_add x;
      '(Ly, y) <- reify monoid_zero monoid_add y;
      T.change (interp M monoid_zero monoid_add Lx x = interp M monoid_zero monoid_add Ly y)
    | [[? g : Prop |- g ]] => fun _ => mfail "Encountered unknown goal: " g
    end.

  Goal forall x y z t, (x + y) + (z + 0 + t) = x + (y + z) + t.
  Proof.
    intros.
    mrun (monoid_lookup).       (* no more arguments *)
    apply: normP Z.add_assoc Z.add_0_l Z.add_0_r _.
    reflexivity.
  Qed.

End Mtac_V2.


(** V3: statically-typed tactics with a certifying reification function. *)
Module Mtac_V3.
  Close Scope tactic_scope.

  (* A certifying lookup function *)
  Definition pos_of {T} {default : T} (var : T) :=
    let go := mfix1 go (L : list T) : M { pos & nth pos L default = var} :=
      mmatch L as L return M { pos & nth pos L default = var} with
      | [? L'] var :: L' =u> M.ret (existT _ 0%nat eq_refl)
      | [? x L'] x :: L' =>
        '(existT _ pos prf) <- go L';
        M.ret (existT _ (S pos) prf)
      (* we no longer need a pattern for the empty list since we'll always find our variable in the tail evar. *)
      (* | _ => mfail "Impossible case: " L *)
      end
    in go.

  (* A certifying reification tactic. With [reify_cert] we can skip unification
     when changing the goal to [interp ... = interp ...]. In more complex
     reflection problems this can save a whole lot of time.

     (We could also use vm_compute to reduce the cost of the unification since
     we may want to introduce a vm_compute cast into the proof term anyway. But
     having it in the proof term does not necessarily mean that one needs to
     actually perform the reduction at tactic runtime. In Mtac2, these two uses
     of vm_compute are othogonal.) *)
  Definition reify_cert {T} (op_zero : T) (op_add : T -> T -> T) (t : T) :
    M { '(L, t') : _ & interp T op_zero op_add L t' = t } :=
    let go :=
      mfix2 go (L : list T) (t : T) : M { t' & interp T op_zero op_add L t' = t } :=
        mmatch t as t return M { t' & interp T op_zero op_add L t' = t } with
        | op_zero => M.ret (existT _ (zero) eq_refl)
        | [? x y] op_add x y =>
          '(existT _ x prfx) <- go L x;
          '(existT _ y prfy) <- go L y;
          prf <- match prfx in _ = X, prfy in _ = Y return M (op_add _ _ = op_add X Y) with
          | eq_refl, eq_refl => M.ret eq_refl
          end;
          M.ret (existT _ (add x y) prf)
        | _ =>
          '(existT _ pos prf) <- pos_of t L;
          M.ret (existT _ (var pos) prf)
      end
    in
    L <- M.evar _;
    '(existT _ t' eq) <- go L t;
    Mtac_V2.end_list L;;        (* put [nil] at the end of [L] *)
    M.ret (existT _ (L, t') eq).


  Import TT. Import TT.notations.
  Open Scope TT.

  (* Let's skip the non-CS version *)
  Definition monoid_lookup : tactic :=
    match_goal with
    | [[? (M : Monoid) (x y : M) |- x = y ]] =>
      '(existT _ (Lx, x) prfx) <- reify_cert monoid_zero monoid_add x;
      '(existT _ (Ly, y) prfy) <- reify_cert monoid_zero monoid_add y;
      (* No need to call [change] since [prfx] and [prfy] prove statically that the goals are convertible *)
      match prfx in _ = X, prfy in _ = Y return ttac (X = Y) with
      | eq_refl, eq_refl => demote (* leave goal unsolved *)
      end
    end.

  Goal forall x y z t, (x + y) + (z + 0 + t) = x + (y + z) + t.
  Proof.
    intros.
    mrun (monoid_lookup).
    apply: normP Z.add_assoc Z.add_0_l Z.add_0_r _.
    reflexivity.
  Qed.

End Mtac_V3.