Simple Mtac2 play ground showing the typed intro issues

mtac2_sandbox.v

From Mtac2 Require Import Mtac2 Ttactics.
Import TT.
Import TT.notations.


(*****************************************************************************)
(** * The sandbox I am playing in                                            *)
(*****************************************************************************)

Parameter A : Type.
Parameter P : A -> Prop.
Definition AP := forall a : A, P a.
Parameter Q R : Prop.
Axiom PQ : AP -> Q.
Axiom QR : Q -> R.


(*****************************************************************************)
(** * Some Mtac definitions and aliases                                      *)
(*****************************************************************************)

(* This passes the dynamic goals in A through to B *) 
Definition lift_MAMB {A B : Type} (f : M A -> M B) : ttac A -> ttac B :=
  (fun att : ttac A => (att >>= (fun '(m: a; adg) => b <- f (M.ret a) ; M.ret (m: b; adg))))%MC.

Definition MAB_MBC_MAC {A B C : Type} (f : M (A -> B)) (g : M (B -> C)) : M (A -> C) :=
  (\nu a : A, g <*> (f <*> (M.ret a)) >>= M.abs_fun a)%MC.

Infix "<;>" := (fun f g => MAB_MBC_MAC g f) (at level 61, left associativity) : M_scope.

Definition MAMB_MBMC_MAMC {A B C : Type} (f : M A -> M B) (g : M B -> M C) : M A -> M C :=
  (fun ma : M A => g (f ma)).

Infix "<;;>" := (fun f g => MAMB_MBMC_MAMC g f) (at level 61, left associativity) : M_scope.

Definition MA_MAB_MB {A B : Type} (ma : M A) (mab : M (A -> B)) : M B := M.fapp mab ma.
Definition TTA_TTAB_TTB {A B : Type} (tta : ttac A) (ttab : ttac (A -> B)) : ttac B := fappgl Mappend ttab tta.


(*****************************************************************************)
(** * Variant with M P -> M Q                                                *)
(*****************************************************************************)

Definition MAMB_APQ : M AP -> M Q := M.fapp (M.ret PQ).
Definition MAMB_QR : M Q  -> M R := M.fapp (M.ret QR).

(* typed tactic - mrun cannot run this *)
Definition TT_MAMB_QR : ttac R := lift_MAMB MAMB_QR TT.demote.
(* tactic - mrun can run this *)
(* Note: this parses without %TT scope, but it is something else then *)
Definition T_MAMB_QR : tactic := (match_goal with | [[ |- R]] => TT_MAMB_QR end)%TT.

Example Test_MAMB_QR : R.
mrun T_MAMB_QR.
(* Works so far *)
Abort.

Definition MAMB_APR : M AP -> M R := MAMB_QR <;;> MAMB_APQ.
Definition TT_MAMB_APR : ttac R := lift_MAMB MAMB_APR TT.demote.
Definition T_MAMB_APR : tactic := (match_goal with | [[ |- R]] => TT_MAMB_APR end)%TT.

Example Test_MAMB_APR : R.
mrun T_MAMB_APR.
(* How to introduce a ? *)
Abort.

Check lift_MAMB MAMB_APR.

Definition TT_MAMB_PR : ttac R := lift_MAMB MAMB_APR (tintro (fun a : A => TT.demote)).
Definition T_MAMB_PR : tactic := (match_goal with | [[ |- R]] => TT_MAMB_PR end)%TT.

Example Test_MAMB_PR : R.
mrun T_MAMB_PR.
(* a is now introduced *)
Abort.

(*****************************************************************************)
(** * Variant with M (P -> Q)                                                *)
(*****************************************************************************)

Definition MAB_APQ : M (AP -> Q) := M.ret PQ.
Definition MAB_QR : M (Q -> R) := M.ret QR.
Definition TT_MAB_QR : ttac R := lift MAB_QR <**> TT.demote.
Definition T_MAB_QR : tactic := (match_goal with | [[ |- R]] => TT_MAB_QR end)%TT.

Example Test_MAB_QR : R.
mrun T_MAB_QR.
(* Nice : stuff is *not* on the shelve, but an immediate goal *)
Abort.

Definition MAB_APR : M (AP -> R) := MAB_QR <;> MAB_APQ.
Definition TT_MAB_APR : ttac R := lift MAB_APR <**> TT.demote.
Definition T_MAB_APR : tactic := (match_goal with | [[ |- R]] => TT_MAB_APR end)%TT.

Example Test_MAB_APR : R.
mrun T_MAB_APR.
(* How to introduce a ? *)
Abort.

Definition TT_MAB_PR : ttac R := lift MAB_APR <**> tintro (fun a : A => TT.demote).
Definition T_MAB_PR : tactic := (match_goal with | [[ |- R]] => TT_MAB_PR end)%TT.

Example Test_MAB_PR : R.
mrun T_MAB_PR.
(* a is now introduced *)
Abort.