Commit 45e1d49b authored by Janno's avatar Janno

Move Mtac code in proofmode/ into separate file.

parent 0ece440c
...@@ -83,6 +83,7 @@ theories/proofmode/intro_patterns.v ...@@ -83,6 +83,7 @@ theories/proofmode/intro_patterns.v
theories/proofmode/spec_patterns.v theories/proofmode/spec_patterns.v
theories/proofmode/sel_patterns.v theories/proofmode/sel_patterns.v
theories/proofmode/tactics.v theories/proofmode/tactics.v
theories/proofmode/tactics_mtac.v
theories/proofmode/notation.v theories/proofmode/notation.v
theories/proofmode/classes.v theories/proofmode/classes.v
theories/proofmode/class_instances.v theories/proofmode/class_instances.v
......
From iris.program_logic Require Export weakestpre. From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import coq_tactics. From iris.proofmode Require Import coq_tactics.
From iris.proofmode Require Export tactics. From iris.proofmode Require Export tactics tactics_mtac.
From iris.heap_lang Require Export tactics lifting. From iris.heap_lang Require Export tactics lifting.
From Mtac2 Require Import Mtac2 Ttactics DecomposeApp MTeleMatch. From Mtac2 Require Import Mtac2 Ttactics DecomposeApp MTeleMatch.
Set Default Proof Using "Type". Set Default Proof Using "Type".
......
...@@ -4,31 +4,10 @@ From iris.base_logic Require Export base_logic big_op. ...@@ -4,31 +4,10 @@ From iris.base_logic Require Export base_logic big_op.
From iris.proofmode Require Export classes notation. From iris.proofmode Require Export classes notation.
From iris.proofmode Require Import class_instances. From iris.proofmode Require Import class_instances.
From stdpp Require Import hlist pretty. From stdpp Require Import hlist pretty.
From Mtac2 Require Import Mtac2 Ttactics DecomposeApp.
Import TT.notations.
Delimit Scope typed_tactic_scope with TT.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Export ident. Export ident.
Set Universe Polymorphism.
Set Polymorphic Inductive Cumulativity.
Unset Universe Minimization ToSet.
Notation env_Reduction := (
RedStrong [rl:RedBeta; RedMatch; RedFix; RedZeta;
RedDeltaOnly
[rl:Dyn (@beq); Dyn (@ascii_beq); Dyn (@string_beq);
Dyn (@env_lookup); Dyn (@env_lookup_delete); Dyn (@env_delete);
Dyn (@env_app); Dyn (@env_replace); Dyn (@env_dom);
Dyn (@env_persistent); Dyn (@env_spatial); Dyn (@env_spatial_is_nil);
Dyn (@envs_dom); Dyn (@envs_lookup); Dyn (@envs_lookup_delete);
Dyn (@envs_delete); Dyn (@envs_snoc); Dyn (@envs_app);
Dyn (@envs_simple_replace); Dyn (@envs_replace); Dyn (@envs_split);
Dyn (@envs_clear_spatial); Dyn (@envs_clear_persistent);
Dyn (@envs_split_go); Dyn (@envs_split)]]
).
Declare Reduction env_cbv := cbv [ Declare Reduction env_cbv := cbv [
option_bind option_bind
beq ascii_beq string_beq positive_beq ident_beq beq ascii_beq string_beq positive_beq ident_beq
...@@ -42,25 +21,6 @@ Ltac env_cbv := ...@@ -42,25 +21,6 @@ Ltac env_cbv :=
match goal with |- ?u => let v := eval env_cbv in u in change v end. match goal with |- ?u => let v := eval env_cbv in u in change v end.
Ltac env_reflexivity := env_cbv; exact eq_refl. Ltac env_reflexivity := env_cbv; exact eq_refl.
Definition env_cbv :=
match_goal with [[? u |- u ] ] => let v := reduce env_Reduction u in T.change v end.
Definition env_reflexivity := env_cbv &> (T <- M.evar Type; t <- M.evar T; T.exact (@eq_refl T t)).
(** * Misc *)
Definition iFresh' (H : string) : gtactic ident :=
match_goal with
| [[? M (Δ : envs M) P |- envs_entails Δ P ]] =>
let Hs := reduce env_Reduction (envs_dom Δ) in (* should we just use RedNF? *)
let H := reduce RedVmCompute ((IAnon (match Hs with
| [] => 1
| _ => 1 + foldr Pos.max 1 (omap (maybe IAnon) Hs)
end))%positive%list) in
T.ret H
| [[? T (G:T) |- G ]] => T.ret (IAnon 1)
end.
Definition iFresh : gtactic ident := iFresh' "~".
(* Tactic Notation tactics cannot return terms *) (* Tactic Notation tactics cannot return terms *)
Ltac iFresh := Ltac iFresh :=
lazymatch goal with lazymatch goal with
...@@ -76,26 +36,6 @@ Ltac iFresh := ...@@ -76,26 +36,6 @@ Ltac iFresh :=
| _ => constr:(IAnon 1) | _ => constr:(IAnon 1)
end. end.
Definition iHypNotFound (s : string) : Exception. exact exception. Qed.
Definition iTypeOf {M} (H : string) : gtactic (option (bool * uPred M)) :=
match_goal with
| [[? (Δ : envs M) P |- envs_entails Δ P ]] =>
let H := reduce RedHNF (envs_lookup H Δ) in
T.ret H
end.
Definition iMissingHyps (Hs : list ident) : gtactic (list ident) :=
M <- M.evar _;
Δ <-
match_goal with
| [[? (Δ : envs M) P |- envs_entails Δ P ]] => T.ret Δ
| [[? b S (Δ : envs M) |- context C [ envs_split b S Δ ] ]] => T.ret Δ
end;
let Hhyps := reduce env_Reduction (envs_dom Δ) in
let H := reduce RedVmCompute (list_difference Hs Hhyps) in
T.ret H.
Ltac iMissingHyps Hs := Ltac iMissingHyps Hs :=
let Δ := let Δ :=
lazymatch goal with lazymatch goal with
...@@ -132,27 +72,6 @@ Proof. split. apply uPred.entails_wand. apply uPred.wand_entails. Qed. ...@@ -132,27 +72,6 @@ Proof. split. apply uPred.entails_wand. apply uPred.wand_entails. Qed.
Instance as_valid_equiv {M} (P Q : uPred M) : AsValid (P Q) (P Q). Instance as_valid_equiv {M} (P Q : uPred M) : AsValid (P Q) (P Q).
Proof. split. apply uPred.equiv_iff. apply uPred.iff_equiv. Qed. Proof. split. apply uPred.equiv_iff. apply uPred.iff_equiv. Qed.
Inductive iGoal : Type :=
| IGoal M : envs M uPred M iGoal.
Definition iPropOf : iGoal -> Prop := fun '(IGoal M Δ P) => @envs_entails M Δ P.
Program Definition iStartProof (C : ig, TT.ttac (iPropOf ig)) : tactic :=
(match_goal with
| [[? (G : Prop) |- G ]] =>
mmatch G in Prop as G' return M (G' *m mlist goal) with
| [#] @envs_entails | M Δ P =n> (C (IGoal M Δ P))
| _ =>
`M P <- M.evar _;
TT.apply (@as_valid_2 G _ P)
<**> TT.by' (T.apply_ || M.failwith "iStartProof: not a uPred")
<**> (TT.apply (@tac_adequate _ _)
<**> C (IGoal M (Envs Enil Enil) P))
end
end%MC
)%TT.
Ltac iStartProof := Ltac iStartProof :=
lazymatch goal with lazymatch goal with
| |- envs_entails _ _ => idtac | |- envs_entails _ _ => idtac
...@@ -219,23 +138,6 @@ Tactic Notation "iExact" constr(H) := ...@@ -219,23 +138,6 @@ Tactic Notation "iExact" constr(H) :=
let P := match goal with |- FromAssumption _ ?P _ => P end in let P := match goal with |- FromAssumption _ ?P _ => P end in
fail "iExact:" H ":" P "does not match goal"]. fail "iExact:" H ":" P "does not match goal"].
Definition iAssumptionCore :=
let find :=
(mfix4 f (A : _) (Γ : env A) (i : ident) (P : A) : M unit :=
<[decapp Γ with (@Esnoc A)]> UniMatchNoRed (
fun Γ j Q =>
mtry M.unify_or_fail UniCoq P Q;; M.unify_or_fail UniCoq i j;; M.ret ()
with | [? T x y] @NotUnifiable T x y => f _ Γ i P end
)
)%MC in
match_goal with
| [[? A i Γp Γs P _unused |- @envs_lookup A i (Envs Γp Γs) = Some (_unused, P) ] ] =>
mif M.is_evar i then
(find _ Γp i P || find _ Γs i P) &> env_reflexivity
else
M.raise DoesNotMatch
end%tactic.
Tactic Notation "iAssumptionCore" := Tactic Notation "iAssumptionCore" :=
let rec find Γ i P := let rec find Γ i P :=
match Γ with match Γ with
......
From iris.proofmode Require Import coq_tactics.
From iris.proofmode Require Export classes notation.
From iris.proofmode Require Import class_instances tactics.
From Mtac2 Require Import Mtac2 Ttactics DecomposeApp.
Import TT.notations.
Delimit Scope typed_tactic_scope with TT.
Set Default Proof Using "Type".
Export ident.
Set Universe Polymorphism.
Set Polymorphic Inductive Cumulativity.
Unset Universe Minimization ToSet.
Notation env_Reduction := (
RedStrong [rl:RedBeta; RedMatch; RedFix; RedZeta;
RedDeltaOnly
[rl:Dyn (@beq); Dyn (@ascii_beq); Dyn (@string_beq);
Dyn (@env_lookup); Dyn (@env_lookup_delete); Dyn (@env_delete);
Dyn (@env_app); Dyn (@env_replace); Dyn (@env_dom);
Dyn (@env_persistent); Dyn (@env_spatial); Dyn (@env_spatial_is_nil);
Dyn (@envs_dom); Dyn (@envs_lookup); Dyn (@envs_lookup_delete);
Dyn (@envs_delete); Dyn (@envs_snoc); Dyn (@envs_app);
Dyn (@envs_simple_replace); Dyn (@envs_replace); Dyn (@envs_split);
Dyn (@envs_clear_spatial); Dyn (@envs_clear_persistent);
Dyn (@envs_split_go); Dyn (@envs_split)]]
).
Definition env_cbv :=
match_goal with [[? u |- u ] ] => let v := reduce env_Reduction u in T.change v end.
Definition env_reflexivity := env_cbv &> (T <- M.evar Type; t <- M.evar T; T.exact (@eq_refl T t)).
(** * Misc *)
Definition iFresh' (H : string) : gtactic ident :=
match_goal with
| [[? M (Δ : envs M) P |- envs_entails Δ P ]] =>
let Hs := reduce env_Reduction (envs_dom Δ) in (* should we just use RedNF? *)
let H := reduce RedVmCompute ((IAnon (match Hs with
| [] => 1
| _ => 1 + foldr Pos.max 1 (omap (maybe IAnon) Hs)
end))%positive%list) in
T.ret H
| [[? T (G:T) |- G ]] => T.ret (IAnon 1)
end.
Definition iFresh : gtactic ident := iFresh' "~".
Definition iHypNotFound (s : string) : Exception. exact exception. Qed.
Definition iTypeOf {M} (H : string) : gtactic (option (bool * uPred M)) :=
match_goal with
| [[? (Δ : envs M) P |- envs_entails Δ P ]] =>
let H := reduce RedHNF (envs_lookup H Δ) in
T.ret H
end.
Definition iMissingHyps (Hs : list ident) : gtactic (list ident) :=
M <- M.evar _;
Δ <-
match_goal with
| [[? (Δ : envs M) P |- envs_entails Δ P ]] => T.ret Δ
| [[? b S (Δ : envs M) |- context C [ envs_split b S Δ ] ]] => T.ret Δ
end;
let Hhyps := reduce env_Reduction (envs_dom Δ) in
let H := reduce RedVmCompute (list_difference Hs Hhyps) in
T.ret H.
Inductive iGoal : Type :=
| IGoal M : envs M uPred M iGoal.
Definition iPropOf : iGoal -> Prop := fun '(IGoal M Δ P) => @envs_entails M Δ P.
Program Definition iStartProof (C : ig, TT.ttac (iPropOf ig)) : tactic :=
(match_goal with
| [[? (G : Prop) |- G ]] =>
mmatch G in Prop as G' return M (G' *m mlist goal) with
| [#] @envs_entails | M Δ P =n> (C (IGoal M Δ P))
| _ =>
`M P <- M.evar _;
TT.apply (@as_valid_2 G _ P)
<**> TT.by' (T.apply_ || M.failwith "iStartProof: not a uPred")
<**> (TT.apply (@tac_adequate _ _)
<**> C (IGoal M (Envs Enil Enil) P))
end
end%MC
)%TT.
Definition iAssumptionCore :=
let find :=
(mfix4 f (A : _) (Γ : env A) (i : ident) (P : A) : M unit :=
<[decapp Γ with (@Esnoc A)]> UniMatchNoRed (
fun Γ j Q =>
mtry M.unify_or_fail UniCoq P Q;; M.unify_or_fail UniCoq i j;; M.ret ()
with | [? T x y] @NotUnifiable T x y => f _ Γ i P end
)
)%MC in
match_goal with
| [[? A i Γp Γs P _unused |- @envs_lookup A i (Envs Γp Γs) = Some (_unused, P) ] ] =>
mif M.is_evar i then
(find _ Γp i P || find _ Γs i P) &> env_reflexivity
else
M.raise DoesNotMatch
end%tactic.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment