Library tacticsforseplog
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 simulation.
Require Import inferules.
Require Import lemmasforseplog.
Set Implicit Arguments.
Tactic Notation "sep" "assocr" "in" hyp (H) :=
apply StarAssocE in H.
Tactic Notation "sep" "assocl" "in" hyp (H) :=
apply StarAssocI in H.
Tactic Notation "sep" "assocr" :=
apply StarAssocI.
Tactic Notation "sep" "assocl" :=
apply StarAssocE.
Tactic Notation "sep" "comm" "in" hyp (H) :=
apply StarComm in H.
Tactic Notation "sep" "comm" :=
apply StarComm.
unfold x
Tactic Notation "unfold" "once" constr (x) :=
unfold x; fold x.
Tactic Notation "unfold" "once" constr (x) "in" hyp (Hp) :=
unfold x in Hp; fold x in Hp.
Tactic Notation "unfold" "once" constr (x) "in" "*" :=
unfold x in *; fold x in *.
Ltac sassocrH H :=
match type of H with
| _ |= (_ ** _) ** _ => sep assocr in H; sassocrH H
| _ => idtac
end.
Ltac sassoclH H :=
match type of H with
| _ |= _ ** (_ ** _) => sep assocl in H; sassoclH H
| _ => idtac
end.
Ltac sassocr :=
match goal with
| |- _ |= (_ ** _) ** _ => sep assocr; sassocr
| _ => idtac
end.
Ltac sassocl :=
match goal with
| |- _ |= _ ** (_ ** _) => sep assocl; sassocl
| _ => idtac
end.
Ltac scommH H :=
match type of H with
| _ |= _ ** _ => sep comm in H
| _ => idtac
end.
Ltac scomm :=
match goal with
| |- _ |= _ ** _ => sep comm
| _ => idtac
end.
Ltac slift n :=
match eval compute in n with
| 0 => fail
| 1 => sassocr
| S ?n´ => sassocr; scomm; slift n´
end.
Ltac sliftH H n :=
match eval compute in n with
| 0 => fail
| 1 => sassocrH H
| S ?n´ => sassocrH H; scommH H; sliftH H n´
end.
Inductive find : Type :=
| some : nat -> find
| none : nat -> find.
Definition myAconj := Aconj.
Ltac hypSearch_Pure´ Hp :=
match Hp with
| ?A ** ?B => match hypSearch_Pure´ A with
| some ?l => constr:(some l)
| none ?l => match hypSearch_Pure´ B with
| some ?r => constr:(some (l+r))
| none ?r => constr:(none (l+r))
end
end
| [| _ |] => constr:(some 1)
| _ => constr:(none 1)
end.
Ltac hypSearch_Pure Hp :=
let x := hypSearch_Pure´ Hp in
eval compute in x.
Ltac hypSearch´ Hp Assn :=
match Hp with
| ?A ** ?B => match hypSearch´ A Assn with
| some ?l => constr:(some l)
| none ?l => match hypSearch´ B Assn with
| some ?r => constr:(some (l+r))
| none ?r => constr:(none (l+r))
end
end
| Assn => constr:(some 1)
| _ => constr:(none 1)
end.
Ltac hypSearch Hp Assn :=
let x := hypSearch´ Hp Assn in
eval compute in x.
Ltac hypSearch_Conj´ Hp :=
match Hp with
| ?A ** ?B => match hypSearch_Conj´ A with
| some ?l => constr:(some l)
| none ?l => match hypSearch_Conj´ B with
| some ?r => constr:(some (l+r))
| none ?r => constr:(none (l+r))
end
end
| _ //\\ _ => constr:(some 1)
| _ => constr:(none 1)
end.
Ltac hypSearch_Conj Hp :=
let x := hypSearch_Conj´ Hp in
eval compute in x.
Ltac hypSearch_Aemp´ Hp :=
match Hp with
| ?A ** ?B => match hypSearch_Aemp´ A with
| some ?l => constr:(some l)
| none ?l => match hypSearch_Aemp´ B with
| some ?r => constr:(some (l+r))
| none ?r => constr:(none (l+r))
end
end
| Aemp => constr:(some 1)
| _ => constr:(none 1)
end.
Ltac hypSearch_Aemp Hp :=
let x := hypSearch_Aemp´ Hp in
eval compute in x.
Ltac hypSearch_Ex´ Hp :=
match Hp with
| ?A ** ?B => match hypSearch_Ex´ A with
| some ?l => constr:(some l)
| none ?l => match hypSearch_Ex´ B with
| some ?r => constr:(some (l+r))
| none ?r => constr:(none (l+r))
end
end
| EX _ , _ => constr:(some 1)
| _ => constr:(none 1)
end.
Ltac hypSearch_Ex Hp :=
let x := hypSearch_Ex´ Hp in
eval compute in x.
Ltac spureH_1 H :=
let s´ := fresh in
let H´ := fresh in
match type of H with
| _ |= ?A => match hypSearch_Pure A with
| some ?n => sliftH H n; eapply StarMono in H;
[ idtac
| intros s´ H´; exact H´
| intros s´ H´; try progress spureH_1 H´; exact H´]
| _ => idtac
end
| _ => fail
end.
Ltac spureH_2 H :=
let s´ := fresh in
let H´ := fresh in
match type of H with
| _ |= [| _ |] //\\ _ => apply ConjPureEL in H;
eapply StarMono in H;
[ idtac
| intros s´ H´; exact H´
| intros s´ H´; try progress spureH_2 H´; exact H´]
| _ |= _ //\\ [| _ |] => apply ConjPureER in H;
eapply StarMono in H;
[ idtac
| intros s´ H´; exact H´
| intros s´ H´; try progress spureH_2 H´; exact H´]
| _ |= ([| _ |] ** _) //\\ _ => apply ConjStarPureEL in H;
eapply StarMono in H;
[ idtac
| intros s´ H´; exact H´
| intros s´ H´; try progress spureH_2 H´; exact H´]
| _ |= _ //\\ ([| _ |] ** _) => apply ConjStarPureER in H;
eapply StarMono in H;
[ idtac
| intros s´ H´; exact H´
| intros s´ H´; try progress spureH_2 H´; exact H´]
| _ |= _ => idtac
| _ => fail
end.
Ltac spureH_3 H :=
let s´ := fresh in
let H´ := fresh in
match type of H with
| _ |= _ //\\ _ => eapply ConjMono in H;
[ idtac
| intros s´ H´; try progress spureH_3 H´; exact H´
| intros s´ H´; try progress spureH_3 H´; exact H´];
cbv beta in H; try progress spureH_2 H
| _ |= _ ** _ => eapply StarMono in H;
[ idtac
| intros s´ H´; try progress spureH_3 H´; exact H´
| intros s´ H´; try progress spureH_3 H´; exact H´];
cbv beta in H; try progress spureH_1 H
| _ |= _ => idtac
| _ => fail
end.
Ltac spureH_4 H :=
let H´ := fresh "H" in
match type of H with
| _ |= [| _ |] => apply EmpPureE in H; destruct H as [H´ H]
| _ |= [| _ |] ** _ => apply StarPureE in H; destruct H as [H´ H];
try progress spureH_4 H
| _ |= _ => idtac
| _ => fail
end.
Ltac spureH H :=
try progress spureH_3 H; cbv beta in H; try progress spureH_4 H.
Ltac spure_1 :=
let s := fresh in
let H := fresh in
match goal with
| |- _ |= ?A => match hypSearch_Pure A with
| some ?n => slift n; eapply StarMono;
[ intros s H; exact H
| intros s H; try progress spure_1; exact H
| idtac]
| _ => idtac
end
| _ => fail
end.
Ltac spure_2 :=
let s := fresh in
let H := fresh in
match goal with
| |- _ |= [| _ |] //\\ _ => apply ConjPureIL; eapply StarMono;
[ intros s H; exact H
| intros s H; try progress spure_2; exact H
| idtac]
| |- _ |= _ //\\ [| _ |] => apply ConjPureIR; eapply StarMono;
[ intros s H; exact H
| intros s H; try progress spure_2; exact H
| idtac]
| |- _ |= ([| _ |] ** _) //\\ _ => apply ConjStarPureIL; eapply StarMono;
[ intros s H; exact H
| intros s H; try progress spure_2; exact H
| idtac]
| |- _ |= _ //\\ ([| _ |] ** _) => apply ConjStarPureIR; eapply StarMono;
[ intros s H; exact H
| intros s H; try progress spure_2; exact H
| idtac]
| |- _ |= _ => idtac
| _ => fail
end.
Ltac spure_3 :=
let s := fresh in
let H := fresh in
match goal with
| |- _ |= _ //\\ _ => eapply ConjMono;
[ intros s H; try progress spure_3; exact H
| intros s H; try progress spure_3; exact H
| idtac];
cbv beta; try progress spure_2
| |- _ |= _ ** _ => eapply StarMono;
[ intros s H; try progress spure_3; exact H
| intros s H; try progress spure_3; exact H
| idtac];
cbv beta; try progress spure_1
| |- _ |= _ => idtac
| _ => fail
end.
Ltac spure_4 :=
match goal with
| |- _ |= [| _ |] => apply EmpPureI; [idtac | idtac]
| |- _ |= [| _ |] ** _ => apply StarPureI; [try progress spure_4 | idtac]
| |- _ |= _ => idtac
| _ => fail
end.
Ltac spure :=
try progress spure_3; cbv beta; try progress spure_4.
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 asrtTree2list´ (Hp:asrtTree) (l:list asrtTree) : list asrtTree :=
match Hp with
| starTree A B => asrtTree2list´ A (asrtTree2list´ B l)
| _ => Hp::l
end.
Definition asrtTree2list (Hp:asrtTree) : list asrtTree :=
asrtTree2list´ Hp nil.
Ltac asrt2list´ Hp l :=
match Hp with
| ?A ** ?B => let rl := asrt2list´ B l in
asrt2list´ A rl
| ?A => constr:(A :: l)
end.
Ltac asrt2list Hp := asrt2list´ Hp (@nil asrt).
Ltac listgoalSearch´ lg Hp n :=
match lg with
| nil => constr:(@None)
| ?a :: ?lg´ => match hypSearch Hp a with
| some _ => constr:(Some n)
| _ => listgoalSearch´ lg´ Hp (S n)
end
end.
Ltac listgoalSearch lg Hp := listgoalSearch´ lg Hp 1.
Ltac goalSearch G Hp :=
let lg := asrt2list G in
let x := listgoalSearch lg Hp in
eval compute in x.
Ltac sclearAempH H :=
match type of H with
| ?s |= ?A => match hypSearch_Aemp A with
| some ?n => sliftH H n;
apply StarEmpEL in H; sclearAempH H
| _ => idtac
end
| _ => fail
end.
Ltac sclearAemp :=
match goal with
| |- ?s |= ?A => match hypSearch_Aemp A with
| some ?n => slift n;
apply StarEmpIL; sclearAemp
| _ => idtac
end
| _ => fail
end.
Ltac sauto´ :=
slift 1;
let s´ := fresh in
let H´ := fresh in
match goal with
| H : ?s |= ?A |- ?s |= ?A => exact H
| H : ?s |= ?X |- ?s |= ?Y =>
match X with
| ?A ** ?B =>
match Y with
| A ** ?D =>
apply StarMono 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]];
sliftH H 1; sauto´
| ?C ** ?D =>
match hypSearch B C with
| some ?n => sliftH H (S n); sauto´
| none _ => match goalSearch D (A ** B) with
| Some ?m => slift (S m); sauto´
| @None => idtac
end
end
| A => apply StarEmpER; sauto´
| ?C => match hypSearch B C with
| some ?n => sliftH H (S n); sauto´
| none _ => idtac
end
end
| ?A =>
match Y with
| A ** ?C => apply StarEmpIR in H; sauto´
| ?B ** ?C => match hypSearch C A with
| some ?n => slift (S n); sauto´
| _ => idtac
end
| ?B => idtac
end
end
| _ => fail
end.
Ltac sauto :=
match goal with
| H : ?s |= _ |- ?s |= _ =>
sliftH H 1; sauto´;
match goal with
| |- _ |= _ => sclearAempH H; sclearAemp
| _ => idtac
end
| _ => idtac
end.
Ltac sautoH H :=
let H´ := fresh in
let typeH := type of H in
assert typeH as H´ by exact H; clear H;
rename H´ into H; sauto.
Fixpoint myAppAssnTree (l m : list asrtTree) : list asrtTree :=
match l with
| nil => m
| a :: l´ => a :: (myAppAssnTree l´ m)
end.
Fixpoint list2asrtTree (l:list asrtTree) : asrtTree :=
match l with
| nil => empTree
| A::nil => A
| empTree::l´ => list2asrtTree l´
| A::l´ => starTree A (list2asrtTree l´)
end.
Fixpoint list2asrtTree_noClearEmp (l:list asrtTree) : asrtTree :=
match l with
| nil => empTree
| A::nil => A
| A::l´ => starTree A (list2asrtTree_noClearEmp l´)
end.
Ltac list2asrt l :=
match l with
| nil => fail 1 "in list2asrt l, l should not be nil"
| ?A :: nil => constr:(A)
| Aemp :: ?l´ => list2asrt l´
| ?A :: ?l´ => let ar := list2asrt l´ in
constr:(A ** ar)
end.
Ltac list2asrt_noClearEmp l :=
match l with
| nil => fail 1 "in list2asrt l, l should not be nil"
| ?A :: nil => constr:(A)
| ?A :: ?l´ => let ar := list2asrt_noClearEmp l´ in
constr:(A ** ar)
end.
Definition myarrow (A B : asrt) := A ==> B.
Lemma ImplMonoL :
forall P Q P´,
myarrow P´ Q -> myarrow P P´ -> myarrow P Q.
Lemma ImplMonoR :
forall P Q Q´,
myarrow P Q´ -> myarrow Q´ Q -> myarrow P Q.
Lemma myAppAssnTree_nil_r :
forall l : list asrtTree,
myAppAssnTree l nil = l.
Lemma myAppAssnTree_assoc :
forall (l m n : list asrtTree),
myAppAssnTree l (myAppAssnTree m n) = myAppAssnTree (myAppAssnTree l m) n.
Lemma asrtTree2list_prop1 :
forall t l,
myAppAssnTree (asrtTree2list´ t nil) l = asrtTree2list´ t l.
Lemma asrtTree2list_prop2 :
forall t1 t2,
myAppAssnTree (asrtTree2list´ t1 nil) (asrtTree2list´ t2 nil) = asrtTree2list´ t1 (asrtTree2list´ t2 nil).
Lemma list2asrtTree_prop1 :
forall a l,
unTree a ** unTree (list2asrtTree l) <==> unTree (list2asrtTree (a::l)).
Lemma list2asrtTree_prop2 :
forall l1 l2,
unTree (list2asrtTree l1) ** unTree (list2asrtTree l2) <==> unTree (list2asrtTree (myAppAssnTree l1 l2)).
Theorem ssimplE :
forall t:asrtTree,
unTree t ==> unTree (list2asrtTree (asrtTree2list t)).
Theorem ssimplI :
forall t:asrtTree,
unTree (list2asrtTree (asrtTree2list t)) ==> unTree t.
Ltac ssimplH_1´ H :=
let s´ := fresh in
let H´ := fresh in
match type of H with
| _ |= Aemp //\\ Aemp => apply Conj2AempE in H
| _ |= _ //\\ _ => eapply ConjMono in H;
[ idtac
| intros s´ H´; try progress ssimplH_1´ H´; exact H´
| intros s´ H´; try progress ssimplH_1´ H´; exact H´];
cbv beta in H
| _ |= _ \\// _ => eapply DisjMono in H;
[ idtac
| intros s´ H´; try progress ssimplH_1´ H´; exact H´
| intros s´ H´; try progress ssimplH_1´ H´; exact H´];
cbv beta in H
| ?s |= ?A => match hypSearch_Conj A with
| some ?n =>
sliftH H n; eapply StarMono in H;
[idtac
| intros s´ H´; try progress ssimplH_1´ H´; fold myAconj in H´; exact H´
| intros s´ H´; exact H´];
cbv beta in H; try progress ssimplH_1´ H
| _ =>
let t := toTree A in
pose (ssimplE t) as H´;
cbv [asrtTree2list asrtTree2list´ list2asrtTree unTree] in H´;
apply H´ in H; clear H´;
try unfold myAconj in H
end
| _ => fail
end.
Ltac ssimplH_1´´ H :=
let H´ := fresh in
match type of H with
| _ |= EX _ , _ => eapply ExProp in H; [idtac | intros ? H´; try progress ssimplH_1´´ H´; exact H´]
| _ |= _ => try progress ssimplH_1´ H
| _ => fail
end.
Ltac ssimplH_1 H :=
try progress ssimplH_1´´ H; cbv beta in H.
Ltac ssimpl_1´ :=
let s := fresh in
let H := fresh in
match goal with
| |- _ |= Aemp //\\ Aemp => apply Conj2AempI
| |- _ |= _ //\\ _ => eapply ConjMono;
[ intros s H; try progress ssimpl_1´; exact H
| intros s H; try progress ssimpl_1´; exact H
| idtac];
cbv beta
| |- _ |= _ \\// _ => eapply DisjMono;
[ intros s H; try progress ssimpl_1´; exact H
| intros s H; try progress ssimpl_1´; exact H
| idtac];
cbv beta
| |- ?s´ |= ?A => match hypSearch_Conj A with
| some ?n => slift n; eapply StarMono;
[ intros s H; try progress ssimpl_1´; fold myAconj; exact H
| intros s H; exact H
| idtac];
cbv beta; try progress ssimpl_1´
| _ =>
let t := toTree A in
pose (ssimplI t) as H;
cbv [asrtTree2list asrtTree2list´ list2asrtTree unTree] in H;
apply H; clear H;
try unfold myAconj
end
| _ => fail
end.
Ltac ssimpl_1´´ :=
let H := fresh "H" in
match goal with
| |- _ |= EX _ , _ =>
eapply ExProp;
[intros ? H; try progress ssimpl_1´´; exact H | idtac]
| |- _ |= _ => try progress ssimpl_1´
end.
Ltac ssimpl_1 :=
try progress ssimpl_1´´; cbv beta.
Ltac ssimplH_2 H :=
let s´ := fresh "s" in
let H´ := fresh "H" in
match type of H with
| ?P ==> ?Q => assert (myarrow P Q) as H´ by (unfold myarrow; apply H);
clear H; rename H´ into H
| _ => fail
end;
eapply ImplMonoL in H; [idtac |
unfold myarrow; intros s´ H´; try progress ssimplH_1 H´; exact H´];
eapply ImplMonoR in H; [idtac |
unfold myarrow; intros s´ H´; try progress ssimpl_1; exact H´];
unfold myarrow in H.
Ltac ssimpl_2 :=
let s := fresh in
let H := fresh in
match goal with
| |- _ ==> _ => intros s H; try progress ssimplH_1 H; try progress ssimpl_1;
generalize dependent H
| _ => fail
end.
Ltac sexistH_1 H :=
let H´ := fresh "H" in
match type of H with
| _ |= EX _ , _ =>
eapply ExProp in H;
[idtac | intros ? H´; try progress sexistH_1 H´; exact H´]
| _ |= (EX _ , _) //\\ _ => apply ConjExEL in H; sexistH_1 H
| _ |= _ //\\ EX _ , _ => apply ConjExER in H; sexistH_1 H
| _ |= (EX _ , _) \\// _ => apply DisjExEL in H; sexistH_1 H
| _ |= _ \\// EX _ , _ => apply DisjExER in H; sexistH_1 H
| _ |= _ => idtac
| _ => fail
end.
Ltac sexistH_2 H :=
try progress sexistH_1 H; cbv beta in H.
Ltac sexistH_3 H :=
let s´ := fresh in
let H´ := fresh "H" in
match type of H with
| _ |= EX _ , _ =>
eapply ExProp in H;
[idtac | intros ? H´; try progress sexistH_3 H´; exact H´]
| _ |= _ //\\ _ => eapply ConjMono in H;
[ idtac
| intros s´ H´; try progress sexistH_3 H´; exact H´
| intros s´ H´; try progress sexistH_3 H´; exact H´];
cbv beta in H; try progress sexistH_2 H
| _ |= ?A => match hypSearch_Ex A with
| some ?n => sliftH H n; apply StarExEL in H; try progress sexistH_3 H
| _ => match hypSearch_Conj A with
| some ?m =>
sliftH H m; eapply StarMono in H;
[idtac
| intros s´ H´; try progress sexistH_3 H´; fold myAconj in H´; exact H´
| intros s´ H´; exact H´];
cbv beta in H; try progress sexistH_3 H
| _ => idtac
end
end
| _ => fail
end.
Ltac sexistH H :=
try progress sexistH_3 H; try unfold myAconj in H; try progress ssimplH_1 H; cbv beta in H.
Ltac sexist_1 :=
let H := fresh in
match goal with
| |- _ |= EX _ , _ =>
eapply ExProp;
[intros ? H; try progress sexist_1; exact H | idtac]
| |- _ |= (EX _ , _) //\\ _ => apply ConjExIL; sexist_1
| |- _ |= _ //\\ EX _ , _ => apply ConjExIR; sexist_1
| |- _ |= (EX _ , _) \\// _ => apply DisjExIL; sexist_1
| |- _ |= _ \\// EX _ , _ => apply DisjExIR; sexist_1
| |- _ |= _ => idtac
| _ => fail
end.
Ltac sexist_2 :=
try progress sexist_1; cbv beta.
Ltac sexist_3 :=
let s := fresh in
let H := fresh in
match goal with
| |- _ |= EX _ , _ =>
eapply ExProp;
[intros ? H; try progress sexist_3; exact H | idtac]
| |- _ |= _ //\\ _ => eapply ConjMono;
[ intros s H; try progress sexist_3; exact H
| intros s H; try progress sexist_3; exact H
| idtac];
cbv beta; try progress sexist_2
| |- _ |= ?A => match hypSearch_Ex A with
| some ?n => slift n; apply StarExIL; try progress sexist_3
| _ => match hypSearch_Conj A with
| some ?m => slift m; eapply StarMono;
[ intros s H; try progress sexist_3; fold myAconj; exact H
| intros s H; exact H
| idtac];
cbv beta; try progress sexist_3
| _ => idtac
end
end
| _ => fail
end.
Ltac sexist :=
try progress sexist_3; try unfold myAconj; try progress ssimpl_1; cbv beta.
Fixpoint listliftn´ (ll rl:list asrtTree) (n:nat) :=
match rl with
| nil => ll
| a::rl´ => match n with
| 0 => a::(myAppAssnTree ll rl´)
| S n´ => listliftn´ (myAppAssnTree 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 => 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 (list2asrtTree (a::l)) <==> unTree (list2asrtTree (list_insert l a n)).
Theorem unTree_prop2 :
forall l1 l2,
listeq l1 l2 -> unTree (list2asrtTree l1) <==> unTree (list2asrtTree 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 (list2asrtTree l) <==> unTree (list2asrtTree (listliftn l n)).
Theorem sliftE :
forall t n,
unTree t ==> unTree (list2asrtTree (listliftn (asrtTree2list t) n)).
Theorem sliftI :
forall t n,
unTree (list2asrtTree (listliftn (asrtTree2list t) n)) ==> unTree t.
Ltac sepliftH´ H n :=
match n with
| 0 => fail
| S ?n´ =>
let H´ := fresh in
match type of H with
| ?s |= ?A =>
let t := toTree A in
pose (H´ := sliftE t n´);
cbv [asrtTree2list asrtTree2list´ listliftn listliftn´ myAppAssnTree list2asrtTree unTree] in H´;
apply H´ in H; clear H´
end
end.
Ltac sepliftH´´ H n :=
let H´ := fresh in
match type of H with
| _ |= EX _, _ =>
eapply ExProp in H;
[idtac | intros ? H´; try progress sepliftH´´ H´ n; exact H´]
| _ |= _ => try progress sepliftH´ H n
end.
Ltac sepliftH H n :=
try progress sepliftH´´ H n; cbv beta in H.
Ltac seplift´ n :=
match n with
| 0 => fail
| S ?n´ =>
let H := fresh in
match goal with
| |- ?s |= ?A =>
let t := toTree A in
pose (H := sliftI t n´);
cbv [asrtTree2list asrtTree2list´ listliftn listliftn´ myAppAssnTree list2asrtTree unTree] in H;
apply H; clear H
end
end.
Ltac seplift´´ n :=
let H := fresh in
match goal with
| |- _ |= EX _ , _ =>
eapply ExProp;
[intros ? H; try progress seplift´´ n; exact H | idtac]
| |- _ |= _ => try progress seplift´ n
| _ => fail
end.
Ltac seplift n :=
try progress seplift´´ n; cbv beta.
Fixpoint listlowern (l: list asrtTree) (n:nat) : list asrtTree :=
match l with
| nil => l
| a::l´ => match n with
| 0 => myAppAssnTree l´ (a::nil)
| S n´ => a::(listlowern l´ n´)
end
end.
Lemma listeq_prop2 :
forall l a, listeq (myAppAssnTree l (a::nil)) (a::l).
Lemma listeq_lowern :
forall l n, listeq (listlowern l n) l.
Theorem slower :
forall l n,
unTree (list2asrtTree l) <==> unTree (list2asrtTree (listlowern l n)).
Theorem slowerE :
forall t n,
unTree t ==> unTree (list2asrtTree (listlowern (asrtTree2list t) n)).
Theorem slowerI :
forall t n,
unTree (list2asrtTree (listlowern (asrtTree2list t) n)) ==> unTree t.
Ltac slowerHn´ H n :=
match n with
| 0 => fail
| S ?n´ =>
let H´ := fresh in
match type of H with
| ?s |= ?A =>
let t := toTree A in
pose (H´ := slowerE t n´);
cbv [asrtTree2list asrtTree2list´ listlowern myAppAssnTree list2asrtTree unTree] in H´;
apply H´ in H; clear H´
end
end.
Ltac slowerHn´´ H n :=
let H´ := fresh "H" in
match type of H with
| _ |= EX _ , _ =>
eapply ExProp in H;
[idtac | intros ? H´; try progress slowerHn´´ H´ n; exact H´]
| _ |= _ => try progress slowerHn´ H n
end.
Ltac slowerHn H n :=
try progress slowerHn´´ H n; cbv beta in H.
Ltac slowern´ n :=
match n with
| 0 => fail
| S ?n´ =>
let H := fresh in
match goal with
| |- ?s |= ?A =>
let t := toTree A in
pose (H := slowerI t n´);
cbv [asrtTree2list asrtTree2list´ listlowern myAppAssnTree list2asrtTree unTree] in H;
apply H; clear H
end
end.
Ltac slowern´´ n :=
let H := fresh "H" in
match goal with
| |- _ |= EX _ , _ =>
eapply ExProp;
[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 => 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 => 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 => 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 (list2asrtTree l) <==> unTree (list2asrtTree (list_getl l l0)).
Theorem srearrE :
forall t l0,
natlist_sort l0 = baseList 0 (length (asrtTree2list t)) ->
unTree t ==> unTree (list2asrtTree (list_getl (asrtTree2list t) l0)).
Theorem srearrI :
forall t l0,
natlist_sort l0 = baseList 0 (length (asrtTree2list t)) ->
unTree (list2asrtTree (list_getl (asrtTree2list t) l0)) ==> unTree t.
Ltac list_filter_minus1 l :=
match l with
| nil => constr:(@nil nat)
| ?a::?l´ => match a with
| 0 => fail
| S ?a´ => let l´´ := list_filter_minus1 l´ in
constr:(a´::l´´)
end
end.
Ltac srearrH´ H lorder :=
let H´ := fresh in
let l := list_filter_minus1 lorder in
match type of H with
| ?s |= ?A =>
let t := toTree A in
pose (srearrE t l) as H´;
cbv [asrtTree2list asrtTree2list´ natlist_sort length baseList] in H´;
cbv [natlist_insert NPeano.Nat.leb NPeano.leb] in H´;
cbv [list_getl list_getn list2asrtTree unTree] in H´;
apply H´ in H; [clear H´ | auto]
end.
Ltac srearrH´´ H lorder :=
let H´ := fresh in
match type of H with
| _ |= EX _ , _ =>
eapply ExProp in H; [idtac | intros ? H´; try progress srearrH´´ H´ lorder; exact H´]
| _ |= _ => try progress srearrH´ H lorder
end.
Ltac srearrH H lorder :=
try progress srearrH´´ H lorder; cbv beta in H.
Ltac srearr´ lorder :=
let H := fresh in
let l := list_filter_minus1 lorder in
match goal with
| |- ?s |= ?A =>
let t := toTree A in
pose (srearrI t l) as H;
cbv [asrtTree2list asrtTree2list´ natlist_sort length baseList] in H;
cbv [natlist_insert NPeano.Nat.leb NPeano.leb] in H;
cbv [list_getl list_getn list2asrtTree unTree] in H;
apply H; [auto | clear H]
end.
Ltac srearr´´ lorder :=
let H := fresh "H" in
match goal with
| |- _ |= EX _ , _ =>
eapply ExProp;
[intros ? H; try progress srearr´´ lorder; exact H | idtac]
| |- _ |= _ => try progress srearr´ lorder
end.
Ltac srearr lorder :=
try progress srearr´´ lorder; cbv beta.
Ltac seplowerHl H l :=
match l with
| nil => idtac
| ?a::?l´ =>
match type of H with
| ?s |= ?A =>
match hypSearch A a with
| none _ => fail
| some ?n => slowerHn´ H n; seplowerHl H l´
end
end
end.
Ltac seplowerHa H a :=
let l := asrt2list a in
seplowerHl H l.
Ltac seplowerl l :=
match l with
| nil => idtac
| ?a::?l´ =>
match goal with
| |- ?s |= ?A =>
match hypSearch A a with
| none _ => fail
| some ?n => slowern´ n; seplowerl l´
end
end
end.
Ltac seplowera a :=
let l := asrt2list a in
seplowerl l.
Ltac sepapplyH´ H H´ :=
let s´ := fresh in
let H´´ := fresh in
match type of H with
| ?s |= ?A => match type of H´ with
| A ==> ?Q =>
apply H´ in H
| ?P ==> ?Q =>
let sn := hypSearch A P in
match sn with
| some ?n => sliftH H n;
eapply StarMono with (P´:=Q) in H;
[idtac | exact H´ | intros s´ H´´; exact H´´]
| _ => idtac
end
end
| _ => fail
end.
Ltac sepapplyH H H´ :=
ssimplH_2 H´;
match type of H´ with
| ?P ==> ?Q => seplowerHa H P;
let P´ := fresh in
remember P as P´; sepapplyH´ H H´; subst P´; ssimplH_1 H
| _ => fail
end.
Ltac sepapply´ H :=
let s´ := fresh in
let H´´ := fresh in
match goal with
| |- ?s |= ?A => match type of H with
| ?P ==> A =>
apply H
| ?P ==> ?Q =>
let sn := hypSearch A Q in
match sn with
| some ?n => slift n;
eapply StarMono with (P´:=Q);
[exact H | intros s´ H´´; exact H´´ | idtac]
| _ => idtac
end
end
| _ => fail
end.
Ltac sepapply H :=
ssimplH_2 H;
match type of H with
| ?P ==> ?Q => seplowera Q;
let Q´ := fresh in
remember Q as Q´; sepapply´ H; subst Q´; ssimpl_1
| _ => fail
end.
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 n := asrtlength´ Hp in
eval compute in (n-1).
Ltac ge_nat x y :=
match y with
| 0 => constr:true
| S ?y´ => match x with
| 0 => constr:false
| S ?x´ => ge_nat x´ y´
end
end.
this sunify_1 works well, but if it fails to find a match,
it takes a long time: o(m^2 * n^2)
Ltac sunify_1´ lh lg m n :=
let s´ := fresh in
let H´ := fresh in
match goal with
| H : ?s |= ?A ** ?B |- ?s |= ?C ** ?D =>
try solve [apply StarMono with (P:=A) (Q:=B);
[ intros s´ H´; exact H´
| intros s´ H´; sassocrH H´; sassocr;
match lh with
| 0 => fail
| S ?x => match lg with
| 0 => fail
| S ?y => sunify_1´ x y x y
end
end
| exact H]];
sassoclH H; scommH H;
match m with
| 0 => sassocl; scomm;
match n with
| 0 => idtac
| S ?n´ => sunify_1´ lh lg lh n´
end
| S ?m´ => sunify_1´ lh lg m´ n
end
| H : ?s |= _ |- ?s |= _ => exact H
| _ => fail
end.
Ltac sunify_1 :=
match goal with
| H : ?s |= ?A |- ?s |= ?B =>
let x := asrtlength A in
let y := asrtlength B in
match ge_nat x y with
| true => try solve [sassocrH H; sassocr; sunify_1´ x y x y]
| false => idtac
end
| _ => fail
end.
let s´ := fresh in
let H´ := fresh in
match goal with
| H : ?s |= ?A ** ?B |- ?s |= ?C ** ?D =>
try solve [apply StarMono with (P:=A) (Q:=B);
[ intros s´ H´; exact H´
| intros s´ H´; sassocrH H´; sassocr;
match lh with
| 0 => fail
| S ?x => match lg with
| 0 => fail
| S ?y => sunify_1´ x y x y
end
end
| exact H]];
sassoclH H; scommH H;
match m with
| 0 => sassocl; scomm;
match n with
| 0 => idtac
| S ?n´ => sunify_1´ lh lg lh n´
end
| S ?m´ => sunify_1´ lh lg m´ n
end
| H : ?s |= _ |- ?s |= _ => exact H
| _ => fail
end.
Ltac sunify_1 :=
match goal with
| H : ?s |= ?A |- ?s |= ?B =>
let x := asrtlength A in
let y := asrtlength B in
match ge_nat x y with
| true => try solve [sassocrH H; sassocr; sunify_1´ x y x y]
| false => idtac
end
| _ => fail
end.
this sunify_2 works, and if it fails to find a match,
it takes shorter time: o(m^2 * n)
Ltac sunify_2´ lh lg m :=
let s´ := fresh in
let H´ := fresh in
match goal with
| H : ?s |= ?A ** ?B |- ?s |= ?C ** ?D =>
try solve [apply StarMono with (P:=A) (Q:=B);
[ intros s´ H´; exact H´
| intros s´ H´; sassocrH H´; sassocr;
match lh with
| 0 => fail
| S ?x => match lg with
| 0 => fail
| S ?y => sunify_2´ x y x
end
end
| exact H]];
match m with
| 0 => idtac
| S ?m´ => sassoclH H; scommH H; sunify_2´ lh lg m´
end
| H : ?s |= _ |- ?s |= _ => exact H
| _ => fail
end.
Ltac sunify_2´´ lh lg n :=
try solve [sunify_2´ lh lg lh];
match n with
| 0 => idtac
| S ?n´ => try solve [sassocl; scomm; sunify_2´´ lh lg n´]
end.
Ltac sunify_2 :=
match goal with
| H : ?s |= ?A |- ?s |= ?B =>
let x := asrtlength A in
let y := asrtlength B in
match ge_nat x y with
| true => try solve [sassocrH H; sassocr; sunify_2´´ x y y]
| false => idtac
end
| _ => fail
end.
Tactic Notation "sep" "unify" :=
sunify_2.
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.
Goal forall {t:Type} (A B C D E F G: t->asrt),
EX x y z m n o, (A x ** B y ** C z ** D m ** E n ** F o)
==>
EX x y z m n o, (B x ** D y ** F z ** C m ** A n ** E o).
Goal forall {t:Type} (A B C D E F: t->asrt) s,
s |= EX x y z m n o, (A x ** B y ** C z ** D m ** E n ** F o)
-> exists P, exists Q, s |= EX x, (P ** B x ** Q).
let s´ := fresh in
let H´ := fresh in
match goal with
| H : ?s |= ?A ** ?B |- ?s |= ?C ** ?D =>
try solve [apply StarMono with (P:=A) (Q:=B);
[ intros s´ H´; exact H´
| intros s´ H´; sassocrH H´; sassocr;
match lh with
| 0 => fail
| S ?x => match lg with
| 0 => fail
| S ?y => sunify_2´ x y x
end
end
| exact H]];
match m with
| 0 => idtac
| S ?m´ => sassoclH H; scommH H; sunify_2´ lh lg m´
end
| H : ?s |= _ |- ?s |= _ => exact H
| _ => fail
end.
Ltac sunify_2´´ lh lg n :=
try solve [sunify_2´ lh lg lh];
match n with
| 0 => idtac
| S ?n´ => try solve [sassocl; scomm; sunify_2´´ lh lg n´]
end.
Ltac sunify_2 :=
match goal with
| H : ?s |= ?A |- ?s |= ?B =>
let x := asrtlength A in
let y := asrtlength B in
match ge_nat x y with
| true => try solve [sassocrH H; sassocr; sunify_2´´ x y y]
| false => idtac
end
| _ => fail
end.
Tactic Notation "sep" "unify" :=
sunify_2.
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.
Goal forall {t:Type} (A B C D E F G: t->asrt),
EX x y z m n o, (A x ** B y ** C z ** D m ** E n ** F o)
==>
EX x y z m n o, (B x ** D y ** F z ** C m ** A n ** E o).
Goal forall {t:Type} (A B C D E F: t->asrt) s,
s |= EX x y z m n o, (A x ** B y ** C z ** D m ** E n ** F o)
-> exists P, exists Q, s |= EX x, (P ** B x ** Q).
Tactic Notation "sep" "pure" "in" hyp (H) :=
match type of H with
| _ |= _ => try progress spureH H
| _ => fail
end.
Tactic Notation "sep" "pure" :=
match goal with
| |- _ |= _ => try progress spure
| _ => fail
end.
Tactic Notation "sep" "simpl" "in" hyp (H) :=
match type of H with
| _ |= _ => try progress (ssimplH_1 H; cbv beta in H)
| _ ==> _ => try progress ssimplH_2 H
| _ => fail
end.
Tactic Notation "sep" "simpl" :=
match goal with
| |- _ |= _ => try progress (ssimpl_1; cbv beta)
| |- _ ==> _ => try progress ssimpl_2
end.
Ltac destructExH H :=
match type of H with
| _ |= EX _ , _ => apply Ex2exists in H; destruct H as [? H]; destructExH H
| _ |= _ => idtac
| _ => fail
end.
Tactic Notation "sep" "exist" "in" hyp (H) :=
try progress (sexistH H; cbv beta in H).
Tactic Notation "sep" "exists" "in" hyp (H) :=
sep exist in H; destructExH H.
Tactic Notation "sep" "exist" :=
try progress (sexist; cbv beta).
Ltac seexists :=
match goal with
| |- _ |= EX _ , _ =>
apply exists2Ex; eexists; seexists
| |- _ |= _ => idtac
| _ => fail
end.
Tactic Notation "sep" "exists" :=
sep exist; seexists.
Ltac sexists x :=
match goal with
| |- _ |= EX _ , _ => apply exists2Ex; exists x
| _ => fail
end.
Tactic Notation "sep" "exists" constr (x1) :=
sep exist; sexists x1.
Tactic Notation "sep" "exists" constr (x1) constr (x2) :=
sep exists x1; sexists x2.
Tactic Notation "sep" "exists" constr (x1) constr (x2) constr (x3) :=
sep exists x1 x2; sexists x3.
Tactic Notation "sep" "exists" constr (x1) constr (x2) constr (x3) constr (x4) :=
sep exists x1 x2 x3; sexists x4.
Tactic Notation "sep" "exists" constr (x1) constr (x2) constr (x3) constr (x4) constr (x5) :=
sep exists x1 x2 x3 x4; sexists x5.
Tactic Notation "sep" "exists" constr (x1) constr (x2) constr (x3) constr (x4) constr (x5)
constr (x6) :=
sep exists x1 x2 x3 x4 x5; sexists x6.
Tactic Notation "sep" "exists" constr (x1) constr (x2) constr (x3) constr (x4) constr (x5)
constr (x6) constr (x7) :=
sep exists x1 x2 x3 x4 x5 x6; sexists x7.
Tactic Notation "sep" "exists" constr (x1) constr (x2) constr (x3) constr (x4) constr (x5)
constr (x6) constr (x7) constr (x8) :=
sep exists x1 x2 x3 x4 x5 x6 x7; sexists x8.
Tactic Notation "sep" "exists" constr (x1) constr (x2) constr (x3) constr (x4) constr (x5)
constr (x6) constr (x7) constr (x8) constr (x9) :=
sep exists x1 x2 x3 x4 x5 x6 x7 x8; sexists x9.
Tactic Notation "sep" "exists" constr (x1) constr (x2) constr (x3) constr (x4) constr (x5)
constr (x6) constr (x7) constr (x8) constr (x9) constr (x10) :=
sep exists x1 x2 x3 x4 x5 x6 x7 x8 x9; sexists x10.
Tactic Notation "sep" "lift" constr (n) "in" hyp (H) :=
try progress (sepliftH H n; cbv beta in H).
Tactic Notation "sep" "lift" constr (n) :=
try progress (seplift n; cbv beta).
Tactic Notation "sep" "lower" constr (n) "in" hyp (H) :=
try progress (slowerHn 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 (srearrH H order; cbv beta in H).
Tactic Notation "sep" "rearr" "with" constr (order) :=
try progress (srearr order; cbv beta).
Tactic Notation "sep" "apply" hyp (H´) "in" hyp (H) :=
try progress sepapplyH H H´.
Tactic Notation "sep" "apply" hyp (H) :=
try progress sepapply H.
Ltac sep_auto :=
intros;
match goal with
| H : ?s |= _ |- ?s |= _ =>
try solve [exact H];
sep exists in H; sep pure 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 exists; sep pure;
match goal with
| |- _ |= _ => sauto; match goal with
| |- _ |= _ => try sep unify
| _ => auto
end
| _ => auto
end
| H : ?s |= _ |- _ =>
first [ solve [eauto]
| sep exists in H; sep pure in H; subst; eauto]
| _ => eauto
end.
Tactic Notation "sep" "auto" := try progress sep_auto.
Ltac sep_auto_with_H H :=
match type of H with
| _ |= _ => let tyH := type of H in
let H´ := fresh in
assert tyH as H´ by exact H; clear H; rename H´ into H;
sep_auto
end.
Tactic Notation "sep" "auto" "with" hyp (H) :=
try progress sep_auto_with_H H.
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 sepliftsH´ H l :=
match l with
| nil => idtac
| ?a::?l´ => sepliftH H a;
sepliftsH´ H l´
end.
Ltac sepliftsH 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
sepliftsH´ H l4.
Ltac seplifts´ l :=
match l with
| nil => idtac
| ?a::?l´ => seplift a;
seplifts´ l´
end.
Ltac seplifts 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
seplifts´ l4.
Tactic Notation "sep" "lifts" constr (l) "in" hyp (H) :=
try progress (sepliftsH H l; cbv beta in H).
Tactic Notation "sep" "lifts" constr (l) :=
try progress (seplifts 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 (list2asrtTree l) <==> unTree (list2asrtTree (empTree::l)).
Theorem saddempR :
forall l,
unTree (list2asrtTree l) <==> unTree (list2asrtTree (list_addempR l)).
Theorem saddempRE :
forall t,
unTree t ==> unTree (list2asrtTree (list_addempR (asrtTree2list t))).
Theorem saddempRI :
forall t,
unTree (list2asrtTree (list_addempR (asrtTree2list t))) ==> unTree t.
Ltac saddEmpHR H :=
let H´ := fresh in
match type of H with
| ?s |= ?A =>
let t := toTree A in
pose (H´ := saddempRE t);
cbv [asrtTree2list asrtTree2list´ list_addempR list2asrtTree unTree] in H´;
apply H´ in H; clear H´
| _ => fail
end.
Ltac saddEmpR :=
let H := fresh in
match goal with
| |- ?s |= ?A =>
let t := toTree A in
pose (H := saddempRI t);
cbv [asrtTree2list asrtTree2list´ list_addempR list2asrtTree 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.