Ltac2 reification of formulas

LtlLtac2.v

From Ltac2 Require Import Ltac2.

Section Ltl.
  Context {X W: Type} (step: X -> W -> X -> W -> Prop).
  Notation XP := (X -> W -> Prop).

  Definition lnext(φ: XP): XP :=
    fun x w => exists x' w', step x w x' w' /\ φ x' w'.
  Arguments lnext: simpl never.
  Opaque lnext.
  
  Inductive Lform :=
  | And: Lform -> Lform -> Lform
  | Next: Lform -> Lform
  | Now: (W -> Prop) -> Lform.
  
  Fixpoint entails(φ : Lform)(x: X)(w: W) : Prop :=
    match φ with
    | And l r => entails l x w /\ entails r x w
    | Next f => lnext (entails f) x w
    | Now p => p w
    end.

  Notation "⊤" := (Now (fun _ => True)).
  Notation "⊥" := (Now (fun _ => False)).
  Ltac2 rec fold_ctl (form: constr): constr :=
    lazy_match! form with
    | lnext ?φ _ _ =>
        let ψ := fold_ctl φ in
        '(entails (Next $ψ))
    | ?l ?x ?w /\ ?r ?x ?w =>
        let l' := fold_ctl l in
        let r' := fold_ctl r in
        '(entails (And $l' $r'))
    | fun _ => False => '(entails ⊥)
    | fun _ => True => '(entails True)
    | entails ?φ => φ
    | ?o => Message.print (Message.of_constr o);
           Control.zero Match_failure
  end.
  
  Context (φ: Lform) (x: X) (w: W).

  Goal entails (Next φ) x w -> False.
    intros H.
    cbn in H.

    (* reify *)
    let ty := Constr.type 'H in
    let ty' := fold_ctl ty in
    assert(H': $ty' x w) by apply H; clear H
  Abort.

End Ltl.