Library seplog_tactics
Require Import Coqlib.
Require Import memory.
Require Import Integers.
Require Import List.
Require Import ZArith.
Require Import language.
Require Import opsem.
Require Import LibTactics.
Require Import assertion.
Require Import BaseAsrtDef.
Require Import inferules.
Require Import seplog_lemmas.
Set Implicit Arguments.
Open Scope nat_scope.
unfold x
Tactic Notation "unfold1" constr (x) :=
unfold x; fold x.
Tactic Notation "unfold1" constr (x) "in" hyp (Hp) :=
unfold x in Hp; fold x in Hp.
Tactic Notation "unfold1" constr (x) "in" "*" :=
unfold x in *; fold x in *.
Ltac sassocr_in H :=
match type of H with
| _ |= (_ ** _) ** _ => apply astar_assoc_elim in H; sassocr_in H
| _ => idtac
end.
Ltac sassocl_in H :=
match type of H with
| _ |= _ ** (_ ** _) => apply astar_assoc_intro in H; sassocr_in H
| _ => idtac
end.
Ltac sassocr :=
match goal with
| |- _ |= (_ ** _) ** _ => apply astar_assoc_intro; sassocr
| _ => idtac
end.
Ltac sassocl :=
match goal with
| |- _ |= _ ** (_ ** _) => apply astar_assoc_elim; sassocl
| _ => idtac
end.
Ltac scomm_in H :=
match type of H with
| _ |= _ ** _ => apply astar_comm in H
| _ => idtac
end.
Ltac scomm :=
match goal with
| |- _ |= _ ** _ => apply astar_comm
| _ => idtac
end.
Tactic Notation "sep" "assocr" "in" hyp (H) :=
sassocr_in H.
Tactic Notation "sep" "assocl" "in" hyp (H) :=
sassocl_in H.
Tactic Notation "sep" "assocr" :=
sassocr.
Tactic Notation "sep" "assocl" :=
sassocl.
Tactic Notation "sep" "comm" "in" hyp (H) :=
scomm_in H.
Tactic Notation "sep" "comm" :=
scomm.
Ltac sliftn n :=
match eval compute in n with
| 0%nat => idtac
| 1%nat => sep assocr
| S ?n´ => sep assocr; sep comm; sliftn n´
end.
Ltac sliftn_in H n :=
match eval compute in n with
| 0%nat => idtac
| 1%nat => sep assocr in H
| S ?n´ => sep assocr in H; sep comm in H; sliftn_in H n´
end.
Inductive find {t:Type} : Type :=
| some : t -> find
| none : t -> find.
Definition myAconj := Aconj.
Inductive pattern : Type :=
| pattern_apure : pattern
| pattern_pure : pattern
| pattern_aconj : pattern
| pattern_adisj : pattern
| pattern_atrue : pattern
| pattern_aemp : pattern
| pattern_aexists : pattern
| pattern_ptrmapsto : pattern
| pattern_lvarmapsto : pattern
| pattern_gvarmapsto : pattern
| pattern_ptrstruct : pattern
| pattern_ptrarray : pattern
| pattern_lvararray : pattern
| pattern_gvararray : pattern
| pattern_aarray : pattern
| pattern_default : pattern
| pattern_absdata : pattern.
Ltac asrt_to_pattern Hp :=
match Hp with
| [| _ |] => constr:(pattern_apure)
| Aie _ => constr:(pattern_pure)
| Ais _ => constr:(pattern_pure)
| ATopis _ => constr:(pattern_pure)
| Aisr _ => constr:(pattern_pure)
| Acs _ => constr:(pattern_pure)
| A_dom_lenv _ => constr:(pattern_pure)
| A_notin_lenv _ => constr:(pattern_pure)
| Alvarenv _ _ _ => constr:(pattern_pure)
| Agvarenv _ _ _ => constr:(pattern_pure)
| <|| _ ||> => constr:(pattern_pure)
| _ //\\ _ => constr:(pattern_aconj)
| _ \\// _ => constr:(pattern_adisj)
| Aemp => constr:(pattern_aemp)
| Atrue => constr:(pattern_atrue)
| Aexists _ => constr:(pattern_aexists)
| PV ?l @ _ |-> _ => constr:(pattern_ptrmapsto, l)
| LV ?x @ _ |-> _ => constr:(pattern_lvarmapsto, x)
| GV ?x @ _ |-> _ => constr:(pattern_gvarmapsto, x)
| Astruct ?l _ _ => constr:(pattern_ptrstruct, l)
| Aarray ?l _ _ => constr:(pattern_ptrarray, l)
| LAarray ?x _ _ => constr:(pattern_lvararray, x)
| GAarray ?x _ _ => constr:(pattern_gvararray, x)
| Aabsdata ?absid _ => constr:(pattern_absdata, absid)
| _ => constr:(pattern_default, Hp)
end.
Ltac find_match´ Hp x :=
match Hp with
| ?A ** ?B => match find_match´ A x with
| some ?a => constr:(some a)
| none ?a => match find_match´ B x with
| some ?b => constr:(some (a + b)%nat)
| none ?b => constr:(none (a + b)%nat)
end
end
| ?A => match asrt_to_pattern A with
| x => constr:(some 1%nat)
| _ => constr:(none 1%nat)
end
end.
Ltac find_match Hp x :=
let y := find_match´ Hp x in
eval compute in y.
Ltac find_match_all Hp A :=
let x := asrt_to_pattern A in
find_match Hp x.
Ltac find_apure Hp := find_match Hp pattern_apure.
Ltac find_pure Hp := find_match Hp pattern_pure.
Ltac find_aconj Hp := find_match Hp pattern_aconj.
Ltac find_aemp Hp := find_match Hp pattern_aemp.
Ltac find_aexists Hp := find_match Hp pattern_aexists.
Ltac find_ptrmapsto Hp l := find_match Hp (pattern_ptrmapsto, l).
Ltac find_lvarmapsto Hp x := find_match Hp (pattern_lvarmapsto, x).
Ltac find_gvarmapsto Hp x := find_match Hp (pattern_gvarmapsto, x).
Ltac find_ptrstruct Hp l := find_match Hp (pattern_ptrstruct, l).
Ltac find_ptrarray Hp l := find_match Hp (pattern_ptrarray, l).
Ltac find_lvararray Hp x := find_match Hp (pattern_lvararray, x).
Ltac find_gvararray Hp x := find_match Hp (pattern_gvararray, x).
Inductive asrtTree : Type :=
| empTree : asrtTree
| trueTree : asrtTree
| starTree : asrtTree -> asrtTree -> asrtTree
| pureTree : Prop -> asrtTree
| baseTree : asrt -> asrtTree.
Ltac toTree Hp :=
match Hp with
| ?A ** ?B => let tA := toTree A in
let tB := toTree B in
constr:(starTree tA tB)
| Aemp => constr:(empTree)
| Atrue => constr:(trueTree)
| [| ?P |] => constr:(pureTree P)
| _ => constr:(baseTree Hp)
end.
Fixpoint unTree (t:asrtTree) : asrt :=
match t with
| empTree => Aemp
| trueTree => Atrue
| starTree A B => unTree A ** unTree B
| pureTree P => [| P |]
| baseTree A => A
end.
Fixpoint asrtTree_to_list´ (Hp:asrtTree) (l:list asrtTree) : list asrtTree :=
match Hp with
| starTree A B => asrtTree_to_list´ A (asrtTree_to_list´ B l)
| _ => Hp::l
end.
Definition asrtTree_to_list (Hp:asrtTree) : list asrtTree :=
asrtTree_to_list´ Hp nil.
Ltac asrt_to_list´ Hp l :=
match Hp with
| ?A ** ?B => let rl := asrt_to_list´ B l in
asrt_to_list´ A rl
| ?A => constr:(A :: l)
end.
Ltac asrt_to_list Hp := asrt_to_list´ Hp (@nil asrt).
Ltac search_match´ lg Hp n :=
match lg with
| nil => constr:(@None)
| ?a :: ?lg´ =>
match asrt_to_pattern a with
| pattern_apure => search_match´ lg´ Hp (S n)
| pattern_pure => search_match´ lg´ Hp (S n)
| _ => match find_match_all Hp a with
| some ?m => constr:(Some (m,n))
| _ => search_match´ lg´ Hp (S n)
end
end
end.
Ltac search_match G Hp :=
let lg := asrt_to_list G in
let x := search_match´ lg Hp 1 in
eval compute in x.
Ltac scancel´ :=
sliftn 1;
let s´ := fresh in
let H´ := fresh in
match goal with
| H : ?s |= ?X |- ?s |= ?Y =>
try solve [ exact H | apply atrue_intro ];
match X with
| ?A ** ?B =>
match Y with
| A ** ?D =>
apply astar_mono with (P:=A) (Q:=B);
[intros s´ H´; exact H´ | idtac | exact H];
first [ clear s H; intros s H
| clear H; first [intros s´ H | intros H]];
sliftn_in H 1; scancel´
| ?C ** ?D =>
match find_match_all B C with
| some ?n => sliftn_in H (S n); scancel´
| none _ => match search_match D (A ** B) with
| Some (_, ?m) => sliftn (S m); scancel´
| @None => idtac
end
end
| A => apply astar_r_aemp_elim; scancel´
| ?C => match find_match_all B C with
| some ?n => sliftn_in H (S n); scancel´
| none _ => idtac
end
end
| ?A =>
match Y with
| A ** ?C => apply astar_r_aemp_intro in H; scancel´
| ?B ** ?C => match find_match_all C A with
| some ?n => sliftn (S n); scancel´
| _ => idtac
end
| ?B => idtac
end
end
| H : (_,_,?m,_,_,?O,_) |= ?X |- (_,_,?m,_,_,?O,_) |= ?Y =>
try solve [ exact H | apply atrue_intro ];
match X with
| ?A ** ?B =>
match Y with
| A ** ?D =>
generalize dependent H;
apply cancellation_rule;
[ sliftn_in H 1; scancel´
| simpl; auto ]
| ?C ** ?D =>
match find_match_all B C with
| some ?n => sliftn_in H (S n); scancel´
| none _ => match search_match D (A ** B) with
| Some (_, ?m) => sliftn (S m); scancel´
| @None => idtac
end
end
| A => apply astar_r_aemp_elim; scancel´
| ?C => match find_match_all B C with
| some ?n => sliftn_in H (S n); scancel´
| none _ => idtac
end
end
| ?A =>
match Y with
| A ** ?C => apply astar_r_aemp_intro in H; scancel´
| ?B ** ?C => match find_match_all C A with
| some ?n => sliftn (S n); scancel´
| _ => idtac
end
| ?B => idtac
end
end
| _ => fail
end.
Ltac sclearemp_in H :=
match type of H with
| _ |= ?A => match find_aemp A with
| some ?n => sliftn_in H n;
match type of H with
| Aemp ** _ =>
apply astar_l_aemp_elim in H; sclearemp_in H
| Aemp => idtac
end
| _ => idtac
end
| _ => fail
end.
Ltac sclearemp :=
match goal with
| |- _ |= ?A => match find_aemp A with
| some ?n => sliftn n;
match goal with
| |- _ |= Aemp **_ =>
apply astar_l_aemp_intro; sclearemp
| |- _ |= Aemp => idtac
end
| _ => idtac
end
| _ => fail
end.
Ltac scancel :=
match goal with
| H : ?s |= _ |- ?s |= _ =>
sliftn_in H 1; scancel´;
match goal with
| |- _ |= _ => sclearemp_in H; sclearemp
| _ => idtac
end
| H : (_,_,?m,_,_,?O,_) |= _ |- (_,_,?m,_,_,?O,_) |= _ =>
sliftn_in H 1; scancel´;
match goal with
| |- _ |= _ => sclearemp_in H; sclearemp
| _ => idtac
end
| _ => idtac
end.
Ltac scancel_with H :=
let H´ := fresh in
let typeH := type of H in
assert typeH as H´ by exact H; clear H;
rename H´ into H; scancel.
Fixpoint myAppAsrtTree (l m : list asrtTree) : list asrtTree :=
match l with
| nil => m
| a :: l´ => a :: (myAppAsrtTree l´ m)
end.
Fixpoint list_to_asrtTree (l:list asrtTree) : asrtTree :=
match l with
| nil => empTree
| A::nil => A
| empTree::l´ => list_to_asrtTree l´
| A::l´ => starTree A (list_to_asrtTree l´)
end.
Fixpoint list_to_asrtTree_simpl (l:list asrtTree) : asrtTree :=
match l with
| nil => empTree
| A::nil => A
| A::l´ => starTree A (list_to_asrtTree_simpl l´)
end.
Ltac list_to_asrt l :=
match l with
| nil => fail 1 "in list_to_asrt l, l should not be nil"
| ?A :: nil => constr:(A)
| Aemp :: ?l´ => list_to_asrt l´
| ?A :: ?l´ => let ar := list_to_asrt l´ in
constr:(A ** ar)
end.
Ltac list_to_asrt_simpl l :=
match l with
| nil => fail 1 "in list_to_asrt l, l should not be nil"
| ?A :: nil => constr:(A)
| ?A :: ?l´ => let ar := list_to_asrt_simpl l´ in
constr:(A ** ar)
end.
Fixpoint listsimplA (l:list asrtTree) (b:bool) : list asrtTree * bool :=
match l with
| nil => (nil, b)
| h::t => match h with
| trueTree => listsimplA t true
| _ => let (l´,b´) := listsimplA t b in
(h::l´,b´)
end
end.
Definition listsimplB (lb : list asrtTree * bool) : list asrtTree :=
let (l,b) := lb in
if b then myAppAsrtTree l (trueTree::nil) else l.
Definition listsimpl (l:list asrtTree) : list asrtTree :=
listsimplB (listsimplA l false).
Lemma myAppAsrtTree_nil_r :
forall l : list asrtTree,
myAppAsrtTree l nil = l.
Lemma myAppAsrtTree_assoc :
forall (l m n : list asrtTree),
myAppAsrtTree l (myAppAsrtTree m n) = myAppAsrtTree (myAppAsrtTree l m) n.
Lemma asrtTree_to_list_prop1 :
forall t l,
myAppAsrtTree (asrtTree_to_list´ t nil) l = asrtTree_to_list´ t l.
Lemma asrtTree_to_list_prop2 :
forall t1 t2,
myAppAsrtTree (asrtTree_to_list´ t1 nil) (asrtTree_to_list´ t2 nil) = asrtTree_to_list´ t1 (asrtTree_to_list´ t2 nil).
Lemma list_to_asrtTree_prop1 :
forall a l,
unTree a ** unTree (list_to_asrtTree l) <==> unTree (list_to_asrtTree (a::l)).
Lemma list_to_asrtTree_simpl_prop1 :
forall a l,
unTree a ** unTree (list_to_asrtTree_simpl l) <==> unTree (list_to_asrtTree_simpl (a::l)).
Lemma list_to_asrtTree_prop2 :
forall l1 l2,
unTree (list_to_asrtTree l1) ** unTree (list_to_asrtTree l2) <==> unTree (list_to_asrtTree (myAppAsrtTree l1 l2)).
Lemma list_to_asrtTree_simpl_prop2 :
forall l1 l2,
unTree (list_to_asrtTree_simpl l1) ** unTree (list_to_asrtTree_simpl l2) <==> unTree (list_to_asrtTree_simpl (myAppAsrtTree l1 l2)).
Lemma myAppAsrtTree_true_r :
forall l : list asrtTree,
unTree (list_to_asrtTree (myAppAsrtTree l (trueTree::nil)))
<==>
unTree (list_to_asrtTree l) ** Atrue.
Theorem ssimplE´ :
forall t:asrtTree,
unTree t ==> unTree (list_to_asrtTree (asrtTree_to_list t)).
Theorem ssimplI´ :
forall t:asrtTree,
unTree (list_to_asrtTree (asrtTree_to_list t)) ==> unTree t.
Theorem ssimplE_simpl :
forall t:asrtTree,
unTree t ==> unTree (list_to_asrtTree_simpl (asrtTree_to_list t)).
Theorem ssimplI_simpl :
forall t:asrtTree,
unTree (list_to_asrtTree_simpl (asrtTree_to_list t)) ==> unTree t.
Lemma listsimplA_prop :
forall l,
listsimplA l true = let (l´,_) := listsimplA l false in
(l´,true).
Lemma list_to_asrtTree_listsimpl :
forall a l,
unTree (list_to_asrtTree (listsimpl (a::l)))
<==>
unTree a ** unTree (list_to_asrtTree (listsimpl l)).
Theorem listsimpl_prop :
forall l,
unTree (list_to_asrtTree l) <==> unTree (list_to_asrtTree (listsimpl l)).
Theorem ssimplE :
forall t : asrtTree,
unTree t ==> unTree (list_to_asrtTree (listsimpl (asrtTree_to_list t))).
Theorem ssimplI :
forall t : asrtTree,
unTree (list_to_asrtTree (listsimpl (asrtTree_to_list t))) ==> unTree t.
Fixpoint listliftn´ (ll rl:list asrtTree) (n:nat) :=
match rl with
| nil => ll
| a::rl´ => match n with
| 0%nat => a::(myAppAsrtTree ll rl´)
| S n´ => listliftn´ (myAppAsrtTree ll (a::nil)) rl´ n´
end
end.
Definition listliftn l n := listliftn´ nil l n.
Fixpoint list_insert (l:list asrtTree) (a:asrtTree) (n:nat) : list asrtTree :=
match l with
| nil => a::nil
| b::l´ => match n with
| 0%nat => a::b::l´
| S n´ => b::(list_insert l´ a n´)
end
end.
Inductive listeq : list asrtTree -> list asrtTree -> Prop :=
| emptylisteq : listeq nil nil
| nonemptylisteq : forall l1 l2 a m n,
listeq l1 l2 -> listeq (list_insert l1 a m) (list_insert l2 a n).
Lemma unTree_prop1 :
forall a l n,
unTree (list_to_asrtTree_simpl (a::l)) <==> unTree (list_to_asrtTree_simpl (list_insert l a n)).
Theorem unTree_prop2 :
forall l1 l2,
listeq l1 l2 -> unTree (list_to_asrtTree_simpl l1) <==> unTree (list_to_asrtTree_simpl l2).
Lemma list_insert_prop1 :
forall l a, list_insert l a 0 = a::l.
Lemma listeq_prop1 :
forall l, listeq l l.
Lemma list_liftn_prop1 :
forall l1 l2 a n,
exists m, list_insert (listliftn´ l1 l2 n) a m = listliftn´ (a::l1) l2 n.
Lemma listeq_liftn :
forall l n,
listeq (listliftn l n) l.
Lemma listeq_comm :
forall l1 l2,
listeq l1 l2 -> listeq l2 l1.
Theorem slift :
forall l n,
unTree (list_to_asrtTree_simpl l) <==> unTree (list_to_asrtTree_simpl (listliftn l n)).
Theorem sliftE :
forall t n,
unTree t ==> unTree (list_to_asrtTree_simpl (listliftn (asrtTree_to_list t) n)).
Theorem sliftI :
forall t n,
unTree (list_to_asrtTree_simpl (listliftn (asrtTree_to_list t) n)) ==> unTree t.
Theorem sliftE´ :
forall t n P,
unTree t //\\ P ==> unTree (list_to_asrtTree_simpl (listliftn (asrtTree_to_list t) n)) //\\ P.
Theorem sliftI´ :
forall t n P,
unTree (list_to_asrtTree_simpl (listliftn (asrtTree_to_list t) n)) //\\ P ==> unTree t //\\ P.
Ltac sepliftn_in´ H n :=
match n with
| 0%nat => idtac 1 "n starts from 1, not 0"; fail 1
| S ?n´ =>
let H´ := fresh in
match type of H with
| _ |= ?A //\\ _ =>
let t := toTree A in
pose (H´ := sliftE´ t n´);
cbv [asrtTree_to_list asrtTree_to_list´ listliftn listliftn´
myAppAsrtTree list_to_asrtTree_simpl unTree] in H´;
apply H´ in H; clear H´
| _ |= ?A =>
let t := toTree A in
pose (H´ := sliftE t n´);
cbv [asrtTree_to_list asrtTree_to_list´ listliftn listliftn´
myAppAsrtTree list_to_asrtTree_simpl unTree] in H´;
apply H´ in H; clear H´
end
| _ => idtac 2 "type of n should be nat"; fail 2
end.
Ltac sepliftn_in´´ H n :=
let H´ := fresh in
match type of H with
| _ |= EX _, _ =>
eapply aexists_prop in H;
[idtac | intros ? H´; try progress sepliftn_in´´ H´ n; exact H´]
| _ |= _ => try progress sepliftn_in´ H n
end.
Ltac sepliftn_in H n :=
try progress sepliftn_in´´ H n; cbv beta in H.
Ltac sepliftn´ n :=
match n with
| 0%nat => fail 1 "n starts from 1, not 0"; fail 1
| S ?n´ =>
let H := fresh in
match goal with
| |- _ |= ?A //\\ _ =>
let t := toTree A in
pose (H := sliftI´ t n´);
cbv [asrtTree_to_list asrtTree_to_list´ listliftn listliftn´ myAppAsrtTree list_to_asrtTree_simpl unTree] in H;
apply H; clear H
| |- _ |= ?A =>
let t := toTree A in
pose (H := sliftI t n´);
cbv [asrtTree_to_list asrtTree_to_list´ listliftn listliftn´ myAppAsrtTree list_to_asrtTree_simpl unTree] in H;
apply H; clear H
end
| _ => fail 2 "type of n should be nat"; fail 2
end.
Ltac sepliftn´´ n :=
let H := fresh in
match goal with
| |- _ |= EX _ , _ =>
eapply aexists_prop;
[intros ? H; try progress sepliftn´´ n; exact H | idtac]
| |- _ |= _ => try progress sepliftn´ n
| _ => fail
end.
Ltac sepliftn n :=
try progress sepliftn´´ n; cbv beta.
Ltac sclearemp_in H ::=
match type of H with
| _ |= Aemp ** _ => apply astar_l_aemp_elim in H; sclearemp_in H
| _ |= Aemp => idtac
| _ |= ?A => match find_aemp A with
| some ?n => sepliftn_in H n;
sclearemp_in H
| _ => idtac
end
end.
Ltac sclearemp ::=
match goal with
| |- _ |= Aemp ** _ => apply astar_l_aemp_intro; sclearemp
| |- _ |= Aemp => idtac
| |- _ |= ?A => match find_aemp A with
| some ?n => sepliftn n;
sclearemp
| _ => idtac
end
end.
Ltac ssimpl_in´ H :=
let s´ := fresh in
let H´ := fresh in
match type of H with
| _ |= Aemp //\\ Aemp =>
apply aconj_2aemp_elim in H
| _ |= _ //\\ _ =>
eapply aconj_mono in H;
[ idtac
| intros s´ H´; try progress ssimpl_in´ H´; exact H´
| intros s´ H´; try progress ssimpl_in´ H´; exact H´];
cbv beta in H
| _ |= ?A =>
match find_aconj A with
| some ?n =>
sepliftn_in H n; eapply astar_mono in H;
[idtac
| intros s´ H´; try progress ssimpl_in´ H´; fold myAconj in H´; exact H´
| intros s´ H´; exact H´];
cbv beta in H; try progress ssimpl_in´ H
| _ =>
let t := toTree A in
pose (ssimplE t) as H´;
cbv [asrtTree_to_list asrtTree_to_list´ listsimpl listsimplA listsimplB
myAppAsrtTree list_to_asrtTree unTree] in H´;
apply H´ in H; clear H´;
try unfold myAconj in H
end
| _ => fail
end.
Ltac ssimpl_in´´ H :=
let H´ := fresh in
match type of H with
| _ |= EX _ , _ => eapply aexists_prop in H; [idtac | intros ? H´; try progress ssimpl_in´´ H´; exact H´]
| _ |= _ => try progress ssimpl_in´ H
| _ => fail
end.
Ltac ssimpl_in H :=
try progress ssimpl_in´´ H; cbv beta in H.
Ltac ssimpl´ :=
let s := fresh in
let H := fresh in
match goal with
| |- _ |= Aemp //\\ Aemp =>
apply aconj_2aemp_intro
| |- _ |= _ //\\ _ =>
eapply aconj_mono;
[ intros s H; try progress ssimpl´; exact H
| intros s H; try progress ssimpl´; exact H
| idtac];
cbv beta
| |- ?s´ |= ?A =>
match find_aconj A with
| some ?n => sepliftn n; eapply astar_mono;
[ intros s H; try progress ssimpl´; fold myAconj; exact H
| intros s H; exact H
| idtac];
cbv beta; try progress ssimpl´
| _ =>
let t := toTree A in
pose (ssimplI t) as H;
cbv [asrtTree_to_list asrtTree_to_list´ listsimpl listsimplA listsimplB
myAppAsrtTree list_to_asrtTree unTree] in H;
apply H; clear H;
try unfold myAconj
end
| _ => fail
end.
Ltac ssimpl´´ :=
let H := fresh "H" in
match goal with
| |- _ |= EX _ , _ =>
eapply aexists_prop;
[intros ? H; try progress ssimpl´´; exact H | idtac]
| |- _ |= _ => try progress ssimpl´
end.
Ltac ssimpl :=
try progress ssimpl´´; cbv beta.
Ltac snormal_in_1 H :=
let H´ := fresh "H" in
match type of H with
| _ |= EX _ , _ =>
eapply aexists_prop in H;
[idtac | intros ? H´; try progress snormal_in_1 H´; exact H´]
| _ |= (EX _ , _) //\\ _ => apply aconj_l_aexists_elim in H; snormal_in_1 H
| _ |= _ //\\ EX _ , _ => apply aconj_r_aexists_elim in H; snormal_in_1 H
| _ |= _ => idtac
| _ => fail
end.
Ltac snormal_in_2 H :=
try progress snormal_in_1 H; cbv beta in H.
Ltac snormal_in_3 H :=
let s´ := fresh in
let H´ := fresh "H" in
match type of H with
| _ |= EX _ , _ =>
eapply aexists_prop in H;
[idtac | intros ? H´; try progress snormal_in_3 H´; exact H´]
| _ |= _ //\\ _ =>
eapply aconj_mono in H;
[ idtac
| intros s´ H´; try progress snormal_in_3 H´; exact H´
| intros s´ H´; try progress snormal_in_3 H´; exact H´];
cbv beta in H; try progress snormal_in_2 H
| _ |= ?A =>
match find_aexists A with
| some ?n => sepliftn_in H n; apply astar_l_aexists_elim in H; try progress snormal_in_3 H
| _ => match find_aconj A with
| some ?m =>
sepliftn_in H m; eapply astar_mono in H;
[idtac
| intros s´ H´; try progress snormal_in_3 H´; fold myAconj in H´; exact H´
| intros s´ H´; exact H´];
cbv beta in H; try progress snormal_in_3 H
| _ => idtac
end
end
| _ => fail
end.
Ltac snormal_in H :=
try progress snormal_in_3 H; try unfold myAconj in H; ssimpl_in H; cbv beta in H.
Ltac snormal_1 :=
let H := fresh in
match goal with
| |- _ |= EX _ , _ =>
eapply aexists_prop;
[intros ? H; try progress snormal_1; exact H | idtac]
| |- _ |= (EX _ , _) //\\ _ => apply aconj_l_aexists_intro; snormal_1
| |- _ |= _ //\\ EX _ , _ => apply aconj_r_aexists_intro; snormal_1
| |- _ |= (EX _ , _) \\// _ => apply adisj_l_aexists_intro; snormal_1
| |- _ |= _ \\// EX _ , _ => apply adisj_r_aexists_intro; snormal_1
| |- _ |= _ => idtac
| _ => fail
end.
Ltac snormal_2 :=
try progress snormal_1; cbv beta.
Ltac snormal_3 :=
let s := fresh in
let H := fresh in
match goal with
| |- _ |= EX _ , _ =>
eapply aexists_prop;
[intros ? H; try progress snormal_3; exact H | idtac]
| |- _ |= _ //\\ _ =>
eapply aconj_mono;
[ intros s H; try progress snormal_3; exact H
| intros s H; try progress snormal_3; exact H
| idtac];
cbv beta; try progress snormal_2
| |- _ |= ?A =>
match find_aexists A with
| some ?n => sepliftn n; apply astar_l_aexists_intro; try progress snormal_3
| _ => match find_aconj A with
| some ?m => sepliftn m; eapply astar_mono;
[ intros s H; try progress snormal_3; fold myAconj; exact H
| intros s H; exact H
| idtac];
cbv beta; try progress snormal_3
| _ => idtac
end
end
| _ => fail
end.
Ltac snormal :=
try progress snormal_3; try unfold myAconj; ssimpl; cbv beta.
Ltac ssplit_apure_in H :=
let H´ := fresh in
match type of H with
| _ |= ?A =>
match find_apure A with
| some ?n =>
sepliftn_in H n;
match type of H with
| _ |= _ ** _ =>
apply astar_l_apure_elim in H;
destruct H as [ H´ H ];
ssplit_apure_in H
| _ |= _ =>
apply apure_elim in H;
destruct H as [ H´ H ]
end
| _ => idtac
end
| _ => fail
end.
Ltac ssplit_pure_in H :=
let H´ := fresh in
match type of H with
| _ |= ?A =>
match find_pure A with
| some ?n =>
sepliftn_in H n;
match type of H with
| _ |= _ ** _ =>
first [ apply astar_l_aie_elim in H
| apply astar_l_ais_elim in H
| apply astar_l_atopis_elim in H
| apply astar_l_aisr_elim in H
| apply astar_l_acs_elim in H
| apply astar_l_adomlenv_elim in H
| apply astar_l_anotinlenv_elim in H
| apply astar_l_alvarenv_elim in H
| apply astar_l_agvarenv_elim in H
| apply astar_l_aop´_elim in H ];
destruct H as [ H´ H ];
ssplit_pure_in H
| _ |= _ =>
first [ apply aie_elim in H
| apply ais_elim in H
| apply atopis_elim in H
| apply aisr_elim in H
| apply acs_elim in H
| apply adomlenv_elim in H
| apply anotinlenv_elim in H
| apply alvarenv_elim in H
| apply agvarenv_elim in H
| apply aop´_elim in H ];
destruct H as [ H´ H ]
end
| _ => idtac
end
| _ => fail
end.
Ltac ssplit_apure :=
let s := fresh in
let H := fresh in
match goal with
| |- _ |= ?A =>
match find_apure A with
| some ?n =>
sepliftn n;
match goal with
| |- _ |= _ ** _ =>
apply astar_l_apure_intro;
[ ssplit_apure | idtac ]
| |- _ |= _ =>
apply apure_intro
end
| _ => idtac
end
| _ => fail
end.
Ltac ssplit_pure :=
let s := fresh in
let H := fresh in
match goal with
| |- _ |= ?A =>
match find_pure A with
| some ?n =>
sepliftn n;
match goal with
| |- _ |= _ ** _ =>
first [apply astar_l_aie_intro
| apply astar_l_ais_intro
| apply astar_l_atopis_intro
| apply astar_l_aisr_intro
| apply astar_l_acs_intro
| apply astar_l_adomlenv_intro
| apply astar_l_anotinlenv_intro
| apply astar_l_alvarenv_intro
| apply astar_l_agvarenv_intro
| apply astar_l_aop´_intro ];
[ ssplit_pure | idtac ]
| |- _ |= _ =>
first [ apply aie_intro
| apply ais_intro
| apply atopis_intro
| apply aisr_intro
| apply acs_intro
| apply adomlenv_intro
| apply anotinlenv_intro
| apply alvarenv_intro
| apply agvarenv_intro
| apply aop´_intro ]
end
| _ => idtac
end
| _ => fail
end.
Fixpoint listlowern (l: list asrtTree) (n:nat) : list asrtTree :=
match l with
| nil => l
| a::l´ => match n with
| 0%nat => myAppAsrtTree l´ (a::nil)
| S n´ => a::(listlowern l´ n´)
end
end.
Lemma listeq_prop2 :
forall l a, listeq (myAppAsrtTree l (a::nil)) (a::l).
Lemma listeq_lowern :
forall l n, listeq (listlowern l n) l.
Theorem slower :
forall l n,
unTree (list_to_asrtTree_simpl l) <==> unTree (list_to_asrtTree_simpl (listlowern l n)).
Theorem slowerE :
forall t n,
unTree t ==> unTree (list_to_asrtTree_simpl (listlowern (asrtTree_to_list t) n)).
Theorem slowerI :
forall t n,
unTree (list_to_asrtTree_simpl (listlowern (asrtTree_to_list t) n)) ==> unTree t.
Theorem slowerE´ :
forall t n P,
unTree t //\\ P ==> unTree (list_to_asrtTree_simpl (listlowern (asrtTree_to_list t) n)) //\\ P.
Theorem slowerI´ :
forall t n P,
unTree (list_to_asrtTree_simpl (listlowern (asrtTree_to_list t) n)) //\\ P ==> unTree t //\\ P.
Ltac slowern_in´ H n :=
match n with
| 0%nat => fail
| S ?n´ =>
let H´ := fresh in
match type of H with
| _ |= ?A //\\ _ =>
let t := toTree A in
pose (H´ := slowerE´ t n´);
cbv [asrtTree_to_list asrtTree_to_list´ listlowern myAppAsrtTree list_to_asrtTree_simpl unTree] in H´;
apply H´ in H; clear H´
| _ |= ?A =>
let t := toTree A in
pose (H´ := slowerE t n´);
cbv [asrtTree_to_list asrtTree_to_list´ listlowern myAppAsrtTree list_to_asrtTree_simpl unTree] in H´;
apply H´ in H; clear H´
end
end.
Ltac slowern_in´´ H n :=
let H´ := fresh "H" in
match type of H with
| _ |= EX _ , _ =>
eapply aexists_prop in H;
[idtac | intros ? H´; try progress slowern_in´´ H´ n; exact H´]
| _ |= _ => try progress slowern_in´ H n
end.
Ltac slowern_in H n :=
try progress slowern_in´´ H n; cbv beta in H.
Ltac slowern´ n :=
match n with
| 0%nat => fail
| S ?n´ =>
let H := fresh in
match goal with
| |- _ |= ?A //\\ _ =>
let t := toTree A in
pose (H := slowerI´ t n´);
cbv [asrtTree_to_list asrtTree_to_list´ listlowern myAppAsrtTree list_to_asrtTree_simpl unTree] in H;
apply H; clear H
| |- _ |= ?A =>
let t := toTree A in
pose (H := slowerI t n´);
cbv [asrtTree_to_list asrtTree_to_list´ listlowern myAppAsrtTree list_to_asrtTree_simpl unTree] in H;
apply H; clear H
end
end.
Ltac slowern´´ n :=
let H := fresh "H" in
match goal with
| |- _ |= EX _ , _ =>
eapply aexists_prop;
[intros ? H; try progress slowern´´ n; exact H | idtac]
| |- _ |= _ => try progress slowern´ n
end.
Ltac slowern n :=
try progress slowern´´ n; cbv beta.
Fixpoint list_getn (l: list asrtTree) (n:nat) : asrtTree :=
match l with
| nil => empTree
| a::l´ => match n with
| 0%nat => a
| S n´ => list_getn l´ n´
end
end.
Fixpoint list_getl (l: list asrtTree) (l0: list nat) : list asrtTree :=
match l0 with
| nil => nil
| a::l0´ => (list_getn l a)::(list_getl l l0´)
end.
Fixpoint baseList (m n:nat) : list nat :=
match n with
| 0%nat => nil
| S n´ => m::baseList (S m) n´
end.
Fixpoint list_dropn (l: list asrtTree) (n:nat) : list asrtTree :=
match l with
| nil => nil
| a::l´ => match n with
| 0%nat => l
| S n´ => list_dropn l´ n´
end
end.
Fixpoint natlist_insert (l: list nat) (x:nat) : list nat :=
match l with
| nil => x::nil
| a::l´ => if NPeano.Nat.leb x a
then x::a::l´
else a::(natlist_insert l´ x)
end.
Fixpoint natlist_sort (l: list nat) : list nat :=
match l with
| nil => nil
| a::l´ => natlist_insert (natlist_sort l´) a
end.
Lemma list_dropn_prop1 :
forall l, list_dropn l (length l) = nil.
Lemma list_dropn_prop2 :
forall l, list_dropn l 0 = l.
Lemma list_dropn_prop3 :
forall l n,
length l > n ->
list_dropn l n = list_getn l n :: list_dropn l (S n).
Lemma list_dropn_prop4 :
forall l n,
length l >= n ->
list_dropn l (length l - n) = list_getl l (baseList (length l - n) n).
Lemma list_getl_prop1:
forall l l0 a, exists n,
list_getl l (natlist_insert l0 a) = list_insert (list_getl l l0) (list_getn l a) n.
Lemma listeq_getl_sort :
forall l l0,
listeq (list_getl l l0) (list_getl l (natlist_sort l0)).
Lemma listeq_getl :
forall l l0,
natlist_sort l0 = baseList 0 (length l) ->
listeq (list_getl l l0) l.
Theorem srearr :
forall l l0,
natlist_sort l0 = baseList 0 (length l) ->
unTree (list_to_asrtTree_simpl l) <==> unTree (list_to_asrtTree_simpl (list_getl l l0)).
Theorem srearrE :
forall t l0,
natlist_sort l0 = baseList 0 (length (asrtTree_to_list t)) ->
unTree t ==> unTree (list_to_asrtTree_simpl (list_getl (asrtTree_to_list t) l0)).
Theorem srearrI :
forall t l0,
natlist_sort l0 = baseList 0 (length (asrtTree_to_list t)) ->
unTree (list_to_asrtTree_simpl (list_getl (asrtTree_to_list t) l0)) ==> unTree t.
Theorem srearrE´ :
forall t l0 P,
natlist_sort l0 = baseList 0 (length (asrtTree_to_list t)) ->
unTree t //\\ P ==> unTree (list_to_asrtTree_simpl (list_getl (asrtTree_to_list t) l0)) //\\ P.
Theorem srearrI´ :
forall t l0 P,
natlist_sort l0 = baseList 0 (length (asrtTree_to_list t)) ->
unTree (list_to_asrtTree_simpl (list_getl (asrtTree_to_list t) l0)) //\\ P ==> unTree t //\\ P.
Ltac list_filter_minus1 l :=
match l with
| nil => constr:(@nil nat)
| ?a::?l´ => match a with
| 0%nat => fail
| S ?a´ => let l´´ := list_filter_minus1 l´ in
constr:(a´::l´´)
end
end.
Ltac srearr_in´ H lorder :=
let H´ := fresh in
let l := list_filter_minus1 lorder in
match type of H with
| _ |= ?A //\\ _ =>
let t := toTree A in
pose (srearrE´ t l) as H´;
cbv [asrtTree_to_list asrtTree_to_list´ natlist_sort length baseList] in H´;
cbv [natlist_insert NPeano.Nat.leb NPeano.leb] in H´;
cbv [list_getl list_getn list_to_asrtTree_simpl unTree] in H´;
apply H´ in H; [clear H´ | auto]
| _ |= ?A =>
let t := toTree A in
pose (srearrE t l) as H´;
cbv [asrtTree_to_list asrtTree_to_list´ natlist_sort length baseList] in H´;
cbv [natlist_insert NPeano.Nat.leb NPeano.leb] in H´;
cbv [list_getl list_getn list_to_asrtTree_simpl unTree] in H´;
apply H´ in H; [clear H´ | auto]
end.
Ltac srearr_in´´ H lorder :=
let H´ := fresh in
match type of H with
| _ |= EX _ , _ =>
eapply aexists_prop in H; [idtac | intros ? H´; try progress srearr_in´´ H´ lorder; exact H´]
| _ |= _ => try progress srearr_in´ H lorder
end.
Ltac srearr_in H lorder :=
try progress srearr_in´´ H lorder; cbv beta in H.
Ltac srearr´ lorder :=
let H := fresh in
let l := list_filter_minus1 lorder in
match goal with
| |- _ |= ?A //\\ _ =>
let t := toTree A in
pose (srearrI´ t l) as H;
cbv [asrtTree_to_list asrtTree_to_list´ natlist_sort length baseList] in H;
cbv [natlist_insert NPeano.Nat.leb NPeano.leb] in H;
cbv [list_getl list_getn list_to_asrtTree_simpl unTree] in H;
apply H; [auto | clear H]
| |- _ |= ?A =>
let t := toTree A in
pose (srearrI t l) as H;
cbv [asrtTree_to_list asrtTree_to_list´ natlist_sort length baseList] in H;
cbv [natlist_insert NPeano.Nat.leb NPeano.leb] in H;
cbv [list_getl list_getn list_to_asrtTree_simpl unTree] in H;
apply H; [auto | clear H]
end.
Ltac srearr´´ lorder :=
let H := fresh "H" in
match goal with
| |- _ |= EX _ , _ =>
eapply aexists_prop;
[intros ? H; try progress srearr´´ lorder; exact H | idtac]
| |- _ |= _ => try progress srearr´ lorder
end.
Ltac srearr lorder :=
try progress srearr´´ lorder; cbv beta.
Tactic Notation "sep" "split" "in" hyp (H) :=
try progress ssplit_apure_in H; try progress ssplit_pure_in H.
Tactic Notation "sep" "split" :=
try progress ssplit_apure; try progress ssplit_pure.
Tactic Notation "sep" "normal" "in" hyp (H) :=
try progress (snormal_in H; cbv beta in H).
Tactic Notation "sep" "normal" :=
try progress (snormal; cbv beta).
Tactic Notation "sep" "lift" constr (n) "in" hyp (H) :=
try progress (sepliftn_in H n; cbv beta in H).
Tactic Notation "sep" "lift" constr (n) :=
try progress (sepliftn n; cbv beta).
Tactic Notation "sep" "lower" constr (n) "in" hyp (H) :=
try progress (slowern_in H n; cbv beta in H).
Tactic Notation "sep" "lower" constr (n) :=
try progress (slowern n; cbv beta).
Tactic Notation "sep" "rearr" "in" hyp (H) "with" constr (order) :=
try progress (srearr_in H order; cbv beta in H).
Tactic Notation "sep" "rearr" "with" constr (order) :=
try progress (srearr order; cbv beta).
Ltac asrtlength´ Hp :=
match Hp with
| ?A ** ?B => let l := asrtlength´ A in
let r := asrtlength´ B in
constr:(l + r)
| _ => constr:1
end.
Ltac asrtlength Hp :=
let x := asrtlength´ Hp in
eval compute in x.
Ltac ge_nat x y :=
match y with
| 0%nat => constr:true
| S ?y´ => match x with
| 0%nat => constr:false
| S ?x´ => ge_nat x´ y´
end
end.
Ltac sunify´ lh lg m :=
let s´ := fresh in
let H´ := fresh in
match goal with
| H : ?s |= ?A ** ?B |- ?s |= ?C ** ?D =>
try solve [ exact H ];
try solve [ apply astar_mono with (P:=A) (Q:=B);
[ intros s´ H´; exact H´
| intros s´ H´; ssimpl_in H; ssimpl;
match lh with
| 0%nat => fail
| S ?x => match lg with
| 0%nat => fail
| S ?y => sunify´ x y x
end
end
| exact H]];
match m with
| 0%nat => idtac
| S ?m´ => sep lower 1 in H; sunify´ lh lg m´
end
| H : ?s |= _ |- ?s |= _ => first [ exact H | apply atrue_intro ]
| _ => fail
end.
Ltac sunify´´ lh lg n :=
try solve [sunify´ lh lg lh];
match n with
| 0%nat => idtac
| S ?n´ => try solve [sep lower 1; sunify´´ lh lg n´]
end.
Ltac sunify :=
match goal with
| H : ?s |= ?A |- ?s |= ?B =>
try solve [ exact H | apply atrue_intro ];
let x := asrtlength A in
let y := asrtlength B in
match ge_nat x y with
| true => try solve [ssimpl_in H; ssimpl; sunify´´ x y y]
| false => idtac
end
| _ => fail
end.
Tactic Notation "sep" "unify" :=
sunify.
Tactic Notation "sep" "unify" "with" hyp (H) :=
let H´ := fresh in
let Hp := type of H in
assert Hp as H´ by exact H;
clear H; rename H´ into H;
sep unify.
sep auto
Ltac sep_destruct H :=
repeat match type of H with
| _ |= EX _, _ => destruct H as [ ? H ]
end.
Tactic Notation "sep" "destruct" hyp(H) := sep_destruct H.
Ltac sep_eexists :=
repeat match goal with
| |- _ |= EX _, _ => eexists
end.
Tactic Notation "sep" "eexists" := sep_eexists.
Ltac sep_pure :=
match goal with
| |- _ |= _ => idtac
| H : _ |= _ |- _ =>
sep normal in H;
sep destruct H;
sep split in H;
subst
| _ => idtac
end;
auto.
Tactic Notation "sep" "pure" := sep_pure.
Ltac can_change_aop_solver := idtac.
Ltac sep_auto :=
intros;
match goal with
| H : ?s |= _ |- ?s |= _ =>
try solve [ exact H | apply atrue_intro ];
sep normal in H;
sep destruct H;
sep split in H; subst;
(let Hp := type of H in
let H´ := fresh in
assert Hp as H´ by exact H; clear H; rename H´ into H);
sep normal;
sep eexists;
sep split;
match goal with
| |- _ |= _ => scancel; sep unify
| _ => sep_pure
end
| H : (?o,?O,?op) |= _ |- (?o,?O,?op´) |= _ =>
try solve [ apply atrue_intro ];
sep normal in H;
sep destruct H;
sep split in H; subst;
(let Hp := type of H in
let H´ := fresh in
assert Hp as H´ by exact H; clear H; rename H´ into H);
sep normal;
sep eexists;
sep split;
match goal with
| |- _ |= _ =>
apply change_aop_rule with (aop := op);
[ scancel; sep unify
| can_change_aop_solver ]
| _ => sep_pure
end
| _ => idtac
end.
Ltac sep_semiauto :=
intros;
match goal with
| H:?s |= _
|- ?s |= _ =>
try (solve [ exact H | apply atrue_intro ]); sep normal in H; sep
destruct H; sep split in H; subst;
repeat match goal with
| H0 : exists _ , _ |- _ => destruct H0
| H0 : _ /\ _ |- _ => destruct H0
end;
(let Hp := type of H in
let H´ := fresh in
assert Hp as H´ by exact H; clear H; rename H´ into H); sep normal;
sep eexists; sep split;
match goal with
| |- _ |= _ => scancel
| _ => sep_pure
end
| H:(?o, ?O, ?op) |= _
|- (?o, ?O, ?op´) |= _ =>
try (solve [ apply atrue_intro ]); sep normal in H; sep destruct H;
sep split in H; subst;
(let Hp := type of H in
let H´ := fresh in
assert Hp as H´ by exact H; clear H; rename H´ into H); sep normal;
sep eexists; sep split;
match goal with
| |- _ |= _ =>
apply change_aop_rule with (aop := op);
[ scancel | can_change_aop_solver ]
| _ => sep_pure
end
| _ => idtac
end.
Ltac sep_semiauto_nosplit :=
intros;
match goal with
| H:?s |= _
|- ?s |= _ =>
try (solve [ exact H | apply atrue_intro ]); sep normal in H; sep
destruct H; (try progress ssplit_apure_in H); subst;
repeat match goal with
| H0 : exists _ , _ |- _ => destruct H0
| H0 : _ /\ _ |- _ => destruct H0
end;
(let Hp := type of H in
let H´ := fresh in
assert Hp as H´ by exact H; clear H; rename H´ into H); sep normal;
sep eexists; ssplit_apure;
match goal with
| |- _ |= _ => scancel
| _ => sep_pure
end
| H:(?o, ?O, ?op) |= _
|- (?o, ?O, ?op´) |= _ =>
try (solve [ apply atrue_intro ]); sep normal in H; sep destruct H;
(try progress ssplit_apure_in H); subst;
(let Hp := type of H in
let H´ := fresh in
assert Hp as H´ by exact H; clear H; rename H´ into H); sep normal;
sep eexists; ssplit_apure;
match goal with
| |- _ |= _ =>
apply change_aop_rule with (aop := op);
[ scancel | can_change_aop_solver ]
| _ => sep_pure
end
| _ => idtac
end.
Tactic Notation "sep" "semiauto" :=
first [ solve [ sep_semiauto; sep_pure ]
| sep_semiauto ].
Tactic Notation "sep" "semiauton" "nosplit" :=
first [ solve [ sep_semiauto_nosplit; sep_pure ]
| sep_semiauto_nosplit ].
Tactic Notation "sep" "auto" :=
first [ solve [ sep_auto; sep_pure ]
| sep_auto ].
sep lift m n o ...
Ltac multiSepLiftInc a l :=
match l with
| nil => constr:(@nil nat)
| ?b::?l´ => let l´´ := multiSepLiftInc a l´ in
let x := constr:(NPeano.Nat.ltb a b) in
match eval compute in x with
| true => constr:(b::l´´)
| false => constr:((S b)::l´´)
end
end.
Ltac multiSepLift l :=
match l with
| nil => constr:(@nil nat)
| ?b::?l´ => let l0 := multiSepLiftInc b l´ in
let l1 := multiSepLift l0 in
constr:(b::l1)
end.
Ltac sepliftsn_in´ H l :=
match l with
| nil => idtac
| ?a::?l´ => sepliftn_in H a;
sepliftsn_in´ H l´
end.
Ltac sepliftsn_in H l :=
let l1 := constr:(rev l) in
let l2 := (eval compute in l1) in
let l3 := multiSepLift l2 in
let l4 := (eval compute in l3) in
sepliftsn_in´ H l4.
Ltac sepliftsn´ l :=
match l with
| nil => idtac
| ?a::?l´ => sepliftn a;
sepliftsn´ l´
end.
Ltac sepliftsn l :=
let l1 := constr:(rev l) in
let l2 := (eval compute in l1) in
let l3 := multiSepLift l2 in
let l4 := (eval compute in l3) in
sepliftsn´ l4.
Tactic Notation "sep" "lifts" constr (l) "in" hyp (H) :=
try progress (sepliftsn_in H l; cbv beta in H).
Tactic Notation "sep" "lifts" constr (l) :=
try progress (sepliftsn l; cbv beta).
add an Aemp to the end of the asrt
Fixpoint list_addempR (l:list asrtTree) : list asrtTree :=
match l with
| nil => empTree::nil
| a::l´ => a::(list_addempR l´)
end.
Lemma listeq_addemp :
forall l,
listeq (empTree::l) (list_addempR l).
Theorem saddempL :
forall l,
unTree (list_to_asrtTree_simpl l) <==> unTree (list_to_asrtTree_simpl (empTree::l)).
Theorem saddempR :
forall l,
unTree (list_to_asrtTree_simpl l) <==> unTree (list_to_asrtTree_simpl (list_addempR l)).
Theorem saddempRE :
forall t,
unTree t ==> unTree (list_to_asrtTree_simpl (list_addempR (asrtTree_to_list t))).
Theorem saddempRI :
forall t,
unTree (list_to_asrtTree_simpl (list_addempR (asrtTree_to_list t))) ==> unTree t.
Theorem saddempRE´ :
forall t P,
unTree t //\\ P ==> unTree (list_to_asrtTree_simpl (list_addempR (asrtTree_to_list t))) //\\ P.
Theorem saddempRI´ :
forall t P,
unTree (list_to_asrtTree_simpl (list_addempR (asrtTree_to_list t))) //\\ P ==> unTree t //\\ P.
Ltac saddEmpHR H :=
let H´ := fresh in
match type of H with
| _ |= ?A //\\ _ =>
let t := toTree A in
pose (H´ := saddempRE´ t);
cbv [asrtTree_to_list asrtTree_to_list´ list_addempR list_to_asrtTree_simpl unTree] in H´;
apply H´ in H; clear H´
| _ |= ?A =>
let t := toTree A in
pose (H´ := saddempRE t);
cbv [asrtTree_to_list asrtTree_to_list´ list_addempR list_to_asrtTree_simpl unTree] in H´;
apply H´ in H; clear H´
| _ => fail
end.
Ltac saddEmpR :=
let H := fresh in
match goal with
| |- _ |= ?A //\\ _ =>
let t := toTree A in
pose (H := saddempRI´ t);
cbv [asrtTree_to_list asrtTree_to_list´ list_addempR list_to_asrtTree_simpl unTree] in H;
apply H; clear H
| |- _ |= ?A =>
let t := toTree A in
pose (H := saddempRI t);
cbv [asrtTree_to_list asrtTree_to_list´ list_addempR list_to_asrtTree_simpl unTree] in H;
apply H; clear H
| _ => fail
end.
Tactic Notation "sep" "add" "emp" "in" hyp (H) :=
saddEmpHR H.
Tactic Notation "sep" "add" "emp" :=
saddEmpR.
sep rewrite n
Ltac srewrite_in´ H Heq :=
match type of H with
| _ |= _ ** _ => let H´ := fresh in
eapply astar_mono in H;
[ idtac
| intros ? H´; srewrite_in´ H´ Heq; exact H´
| intros ? H´; srewrite_in´ H´ Heq; exact H´]
| _ |= _ //\\ _ => let H´ := fresh in
eapply aconj_mono in H;
[ idtac
| intros ? H´; srewrite_in´ H´ Heq; exact H´
| intros ? H´; srewrite_in´ H´ Heq; exact H´]
| _ |= [| ?x = ?y |] => match type of Heq with
| (x = y) => idtac
| _ => try rewrite Heq in H
end
| _ |= _ => try rewrite Heq in H
end.
Ltac srewriten_in´ H n :=
let H´ := fresh in
let newH := fresh in
let Heq := fresh in
match type of H with
| _ |= EX _ , _ =>
eapply aexists_prop in H; [idtac | intros ? H´; srewriten_in´ H´ n; exact H´]
| _ |= _ =>
let x := type of H in
assert x as newH by exact H;
sep lift n in newH;
match type of newH with
| _ |= [| ?x = ?y |] ** _ //\\ _ =>
let newH´ := fresh in
destruct newH as [ newH newH´ ]; clear newH´;
apply astar_l_apure_elim in newH; destruct newH as [ Heq newH ];
clear newH; srewrite_in´ H Heq; clear Heq
| _ |= [| ?x = ?y |] //\\ _ => clear newH
| _ |= [| ?x = ?y |] ** _ =>
apply astar_l_apure_elim in newH; destruct newH as [ Heq newH ];
clear newH; srewrite_in´ H Heq; clear Heq
| _ |= [| ?x = ?y |] => clear newH
end
end.
Ltac srewriten_in H n :=
srewriten_in´ H n; cbv beta in H.
Tactic Notation "sep" "rewrite" constr(n) "in" hyp(H) :=
srewriten_in H n.
Ltac srewrite_pure_H´´ H H´ :=
let H´´ := fresh in
match type of H´ with
| _ |= ?P =>
match find_apure P with
| some ?n => sep lift n in H´;
match type of H´ with
| _ |= [| _ = _ |] ** _ =>
apply astar_l_apure_elim in H´; destruct H´ as [H´´ H´];
srewrite_in´ H H´´; clear H´´; srewrite_pure_H´´ H H´
| _ |= [| _ |] ** _ =>
apply astar_l_apure_elim in H´; destruct H´ as [H´´ H´];
clear H´´; srewrite_pure_H´´ H H´
| _ |= [| _ = _ |] =>
apply apure_elim in H´; destruct H´ as [H´´ H´];
srewrite_in´ H H´´; clear H´´ H´
| _ |= [| _ |] => clear H´
end
| _ => clear H´
end
end.
Ltac srewrite_pure_H´ H :=
let H´ := fresh in
let newH := fresh in
match type of H with
| _ |= EX _ , _ =>
eapply aexists_prop in H; [idtac | intros ? H´; srewrite_pure_H´ H´; exact H´]
| _ |= _ =>
let x := type of H in
assert x as newH by exact H;
srewrite_pure_H´´ H newH
end.
Ltac srewrite_pure_H H :=
srewrite_pure_H´ H; cbv beta in H.
Tactic Notation "sep" "rewrite" "pure" "in" hyp(H) :=
srewrite_pure_H H.
sep destruct
Ltac sdestroy_in´ H :=
match type of H with
| _ |= _ //\\ _ => let H1 := fresh in
let H2 := fresh in
destruct H as [ H1 H2 ];
sdestroy_in´ H1; sdestroy_in´ H2
| _ |= _ ** _ => apply astar_prop in H; do 2 destruct H as [ ? H ];
let H1 := fresh in
let H2 := fresh in
destruct H as [ H1 H2 ];
sdestroy_in´ H1; sdestroy_in´ H2
| _ |= _ => idtac
end.
Ltac sdestroy_in H :=
sep normal in H;
sep destruct H;
sep split in H;
sdestroy_in´ H.
Tactic Notation "sep" "destroy" hyp(H) := sdestroy_in H.
advanced scancel
Lemma cancel_lvarmapsto :
forall v1 v2 x t P Q,
(P ==> Q) ->
v1 = v2 ->
LV x @ t |-> v1 ** P ==> LV x @ t |-> v2 ** Q.
Lemma cancel_gvarmapsto :
forall v1 v2 x t P Q,
(P ==> Q) ->
v1 = v2 ->
GV x @ t |-> v1 ** P ==> GV x @ t |-> v2 ** Q.
Lemma cancel_ptrmapsto :
forall v1 v2 l t P Q,
(P ==> Q) ->
v1 = v2 ->
PV l @ t |-> v1 ** P ==> PV l @ t |-> v2 ** Q.
Lemma cancel_ptrstruct :
forall ls1 ls2 l t P Q,
(P ==> Q) ->
ls1 = ls2 ->
Astruct l t ls1 ** P ==> Astruct l t ls2 ** Q.
Lemma cancel_ptrarray :
forall ls1 ls2 l t P Q,
(P ==> Q) ->
ls1 = ls2 ->
Aarray l t ls1 ** P ==> Aarray l t ls2 ** Q.
Lemma cancel_lvararray :
forall ls1 ls2 x t P Q,
(P ==> Q) ->
ls1 = ls2 ->
LAarray x t ls1 ** P ==> LAarray x t ls2 ** Q.
Lemma cancel_gvararray :
forall ls1 ls2 x t P Q,
(P ==> Q) ->
ls1 = ls2 ->
GAarray x t ls1 ** P ==> GAarray x t ls2 ** Q.
Lemma cancel_absdata :
forall absdataid absdata1 absdata2 P Q,
(P ==> Q) ->
absdata1 = absdata2 ->
Aabsdata absdataid absdata1 ** P ==> Aabsdata absdataid absdata2 ** Q.
Ltac cancel_same´ :=
let s´ := fresh in
let H´ := fresh in
match goal with
| H : ?s |= LV ?x @ _ |-> _ ** _ |- ?s |= LV ?x @ _ |-> _ ** _ =>
lets H´ : H;
generalize dependent H; apply cancel_lvarmapsto;
[ clear H´; first [ clear s; intros s H | intros s´ H ] | rename H´ into H; auto ]
| H : ?s |= GV ?x @ _ |-> _ ** _ |- ?s |= GV ?x @ _ |-> _ ** _ =>
lets H´ : H;
generalize dependent H; apply cancel_gvarmapsto;
[ clear H´; first [ clear s; intros s H | intros s´ H ] | rename H´ into H; auto ]
| H : ?s |= PV ?l @ _ |-> _ ** _ |- ?s |= PV ?l @ _ |-> _ ** _ =>
lets H´ : H;
generalize dependent H; apply cancel_ptrmapsto;
[ clear H´; first [ clear s; intros s H | intros s´ H ] | rename H´ into H; auto ]
| H : ?s |= Astruct ?l _ _ ** _ |- ?s |= Astruct ?l _ _ ** _ =>
lets H´ : H;
generalize dependent H; apply cancel_ptrstruct;
[ clear H´; first [ clear s; intros s H | intros s´ H ] | rename H´ into H; auto ]
| H : ?s |= Aarray ?l _ _ ** _ |- ?s |= Aarray ?l _ _ ** _ =>
lets H´ : H;
generalize dependent H; apply cancel_ptrarray;
[ clear H´; first [ clear s; intros s H | intros s´ H ] | rename H´ into H; auto ]
| H : ?s |= LAarray ?x _ _ ** _ |- ?s |= LAarray ?x _ _ ** _ =>
lets H´ : H;
generalize dependent H; apply cancel_lvararray;
[ clear H´; first [ clear s; intros s H | intros s´ H ] | rename H´ into H; auto ]
| H : ?s |= GAarray ?x _ _ ** _ |- ?s |= GAarray ?x _ _ ** _ =>
lets H´ : H;
generalize dependent H; apply cancel_gvararray;
[ clear H´; first [ clear s; intros s H | intros s´ H ] | rename H´ into H; auto ]
| H : ?s |= Aabsdata ?id _ ** _ |- ?s |= Aabsdata ?id _ ** _ =>
lets H´ : H;
generalize dependent H; apply cancel_absdata;
[ clear H´; first [ clear s; intros s H | intros s´ H ] | rename H´ into H; auto ]
| H : ?s |= ?A ** _ |- ?s |= ?A ** _ =>
generalize dependent H; apply astar_mono;
[ intros s´ H; exact H | first [ clear s; intros s H | intros s´ H ] ]
end.
Ltac cancel_same :=
match goal with
| H : ?s |= ?X |- ?s |= ?Y =>
try solve [ exact H | apply atrue_intro ];
match search_match Y X with
| Some (?m,?n) =>
sep lift m in H; sep lift n;
match goal with
| H : ?s |= ?A ** ?B |- ?s |= ?C ** ?D =>
cancel_same´; [ cancel_same | idtac .. ]
| H : ?s |= ?A ** ?B |- ?s |= ?C =>
apply astar_r_aemp_elim; cancel_same´; [ cancel_same | idtac .. ]
| H : ?s |= ?A |- ?s |= ?C ** ?D =>
apply astar_r_aemp_intro in H; cancel_same´; [ cancel_same | idtac .. ]
| H : ?s |= ?A |- ?s |= ?C =>
apply astar_r_aemp_intro in H; apply astar_r_aemp_elim;
cancel_same´; [ cancel_same | idtac .. ]
end
| @None => idtac
end
end.
Ltac scancel´ ::= cancel_same.
Ltac scancel ::=
match goal with
| H:?s |= _ |- ?s |= _ =>
sep normal in H; sep normal;
scancel´;
match goal with
| |- _ |= _ => sclearemp_in H; sclearemp
| _ => idtac
end
| _ => idtac
end.
Ltac sep_cancel m n :=
match goal with
| H: ?s |= _ |- ?s |= _ =>
sep lift m in H;
sep lift n;
match goal with
| H : ?s |= ?A ** ?B |- ?s |= ?C ** ?D =>
generalize dependent H; apply astar_mono;
[ intros s´ H; exact H | first [ clear s; intros s H | intros s´ H ] ]
| H : ?s |= ?A ** ?B |- ?s |= ?C =>
apply astar_r_aemp_elim;
generalize dependent H; apply astar_mono;
[ intros s´ H; exact H | first [ clear s; intros s H | intros s´ H ] ]
| H : ?s |= ?A |- ?s |= ?C ** ?D =>
apply astar_r_aemp_intro in H;
generalize dependent H; apply astar_mono;
[ intros s´ H; exact H | first [ clear s; intros s H | intros s´ H ] ]
| H : ?s |= ?A |- ?s |= ?C =>
exact H
end
end.
Tactic Notation "sep" "cancel" constr(m) constr(n) :=
sep_cancel m n.
Ltac find_match_context´ Hp x :=
match Hp with
| ?A ** ?B =>
match find_match_context´ A x with
| some ?a => constr:(some a)
| none ?a =>
match find_match_context´ B x with
| some ?b => constr:(some (a + b)%nat)
| none ?b => constr:(none (a + b)%nat)
end
end
| context [x] => constr:(some 1%nat)
| _ => constr:(none 1%nat)
end.
Ltac find_match_context Hp x :=
let y := find_match_context´ Hp x in
eval compute in y.
Ltac sep_cancel_context x :=
match goal with
| H: ?s |= ?P |- ?s |= ?Q =>
match find_match_context P x with
| none _ => fail 1
| some ?m =>
match find_match_context Q x with
| none _ => fail 2
| some ?n =>
sep cancel m n
end
end
end.
Tactic Notation "sep" "cancel" constr(x) :=
sep_cancel_context x.
Ltac asrt_get_after_n p n :=
match n with
| 0%nat => constr:(Some p)
| S ?n´ =>
match p with
| ?p´ ** ?q´ => asrt_get_after_n q´ n´
| _ => constr:(@None)
end
end.
Ltac sep_remember_in H l :=
sep lifts l in H;
let x := constr:(length l) in
let y := (eval compute in x) in
let a := fresh in
match type of H with
| _ |= ?p =>
match asrt_get_after_n p y with
| @None => fail 1
| Some ?p´ => remember p´ as a
end
end.
Ltac sep_remember l :=
sep lifts l;
let x := constr:(length l) in
let y := (eval compute in x) in
let a := fresh in
match goal with
| |- _ |= ?p =>
match asrt_get_after_n p y with
| @None => fail 1
| Some ?p´ => remember p´ as a
end
end.
Tactic Notation "sep" "remember" constr(l) "in" hyp(H) :=
sep_remember_in H l.
Tactic Notation "sep" "remember" constr(l) :=
sep_remember l.
Ltac sep_destroy´ H :=
match type of H with
| _ |= _ ** _ => apply astar_prop in H; do 2 destruct H as [ ? H ];
let H1 := fresh in
let H2 := fresh in
destruct H as [ H1 H2 ];
sep_destroy´ H1; sep_destroy´ H2
| _ |= _ => idtac
end.
Ltac sep_destroy H :=
sep normal in H;
sep destruct H;
sep split in H;
sep_destroy´ H.
Tactic Notation "sep" "destroy" hyp(H) :=
sep_destroy H.