Library Mtac2Tests.lift

From Mtac2 Require Import Mtac2.

Import M.

Require Import Lists.List.
Import ListNotations.

Set Use Unicoq.

Structure execV {A} (f : M A) B := ExecV { value : B } .

Canonical Structure the_value {A} (f : M A) v := ExecV _ f (lift f v) v.

Arguments value {A} f {B} {e}.

Definition exec {A} (f : M A) {v:A} : lift f v := v.

Goal True.
refine (let H := _ in let _ : value (ret I) = H := eq_refl in H).
Qed.

Goal True.
refine (exec (print "hola";; ret I)).
Qed.

Goal True.
refine (exec (raise exception)).
Abort.
Notation "'[ex' t ']'" := (exec t) (at level 0).

Goal [ex ret True] = True.
  unfold exec.
  reflexivity.
Qed.
Import M.notations.
Definition silly :=
  fix f (n: nat) : M Prop :=
    match n with
    | 0 => ret True
    | S n' => f n' >>= fun r=>ret (True -> r)
    end.

Goal [ex silly 3] : _.   unfold exec.
Abort.