text:
(* Narjes Jomaa and David Nowak,
   Pip code refactored by Mohamed Sami Cherif *)
(** * Summary
    This file contains required lemmas to help in proving some properties
    on our dependent types defined into [Model.ADT] *)
Require Import Lib Pip_state Pip_stateLib Pip_Prop List.
Require Import Coq.Logic.ProofIrrelevance Omega Bool.

(** ADT : level **)
Lemma levelEqBEqNatTrue :
forall l l' : level, Level.eqb l l' = true -> l = l' .
 Proof.
 intros l l' H.
 unfold Level.eqb in H.
 apply beq_nat_true in H.
 destruct l.
 destruct l'. simpl in *.
 subst.
 assert (Hl = Hl0).
 apply proof_irrelevance. subst. intuition.
Qed.

Lemma levelEqBEqNatFalse :
forall l ,
Level.eqb l fstLevel = false -> l > fstLevel.
Proof.
intros.
unfold Level.eqb in H.
apply beq_nat_false in H.
unfold fstLevel in *.
unfold CLevel in *.
case_eq (lt_dec 0 nbLevel).
intros.
rewrite H0 in *.
simpl in *. omega.
intros.
assert (0 < nbLevel).
apply nbLevelNotZero.
contradict H1.
intuition.
Qed.

Lemma levelEqBEqNatFalse0 :
forall l ,
Level.eqb l fstLevel = false -> l > 0.
Proof.
intros.
unfold Level.eqb in H.
apply beq_nat_false in H.
unfold fstLevel in H.
unfold CLevel in H.
case_eq (lt_dec 0 nbLevel).
intros.
rewrite H0 in H.
simpl in *. omega.
intros.
assert (0 < nbLevel).
apply nbLevelNotZero.
contradict H1.
intuition.
Qed.

Lemma levelEqBEqNatTrue0 :
forall l ,
Level.eqb l fstLevel = true -> l <= 0.
Proof.
intros.
unfold Level.eqb in H.
apply beq_nat_true in H.
unfold fstLevel in H.
unfold CLevel in H.
case_eq (lt_dec 0 nbLevel).
intros.
rewrite H0 in H.
simpl in *. omega.
intros.
assert (0 < nbLevel).
apply nbLevelNotZero.
contradict H1.
intuition.
Qed.

Lemma levelPredNone nbL:
Level.eqb nbL fstLevel = false ->
Level.pred nbL <> None.
Proof.
intros.
unfold Level.pred.
case_eq(gt_dec nbL 0); intros.
unfold not; intros.
inversion H1.
apply levelEqBEqNatFalse0 in H.
omega.
Qed.

Lemma levelPredLt nbL l :
Level.eqb nbL fstLevel = false ->
Level.pred nbL = Some l ->
l < nbL.
Proof.
intros.
unfold Level.pred in *.
case_eq(gt_dec nbL 0); intros.
rewrite H1 in *.
inversion H0.
simpl in *.
omega.
apply levelEqBEqNatFalse0 in H.
omega.
Qed.

Lemma CLevel0_r :  forall l : level,l - CLevel 0 = l.
Proof.
unfold CLevel.
case_eq (lt_dec 0 nbLevel).
intros.
simpl. omega.
intros.
assert (0 < nbLevel).
apply nbLevelNotZero. omega.
Qed.

Lemma CLevelIdentity : forall l : level, CLevel (l - CLevel 0) = l.
Proof.
intros l.
rewrite CLevel0_r. destruct l.
simpl.
unfold CLevel.
case_eq(lt_dec l nbLevel).
intros. simpl.
assert ( Hl = Pip_state.CLevel_obligation_1 l l0).
apply proof_irrelevance.
subst. reflexivity.
intros.
contradict H.
omega.
Qed.

Lemma CLevelIdentity1 : forall l : level, CLevel l  = l.
Proof.
intros l.
unfold CLevel.
case_eq(lt_dec l nbLevel).
intros. simpl.
destruct l.
simpl.
f_equal.
apply proof_irrelevance.
subst.
intros.
destruct l.
simpl in *.
omega.
Qed.

Lemma CLevelIdentityLe :
forall a , a < nbLevel ->  a <= CLevel a.
Proof.
intros.
unfold CLevel.
case_eq (lt_dec a nbLevel); intros.
simpl; omega.
now contradict H.
Qed.

Lemma levelPredMinus1: forall l l' , Level.eqb l fstLevel = false -> Level.pred l = Some l' -> l' = CLevel (l - 1).
Proof.
intros.
unfold Level.pred  in *.
assert (l > 0).
{ apply levelEqBEqNatFalse0.
  assumption. }
case_eq (gt_dec l 0).
* intros.
  rewrite H2 in H0.
  inversion H0.
  unfold CLevel.
  case_eq (lt_dec (l - 1) nbLevel).
  intros. subst.
  assert (Pip_state.CLevel_obligation_1 (l - 1) l0  = Pip_stateLib.Level.pred_obligation_1 l g ).
  apply proof_irrelevance.
  rewrite H4. reflexivity.
  intros.
  destruct l.
  subst.
  simpl in *.
  contradict H3.
  omega.
* intros.
  contradict H1.
  assumption.
Qed.

Lemma levelEqNat :
forall a b , a < nbLevel -> b < nbLevel -> CLevel a = CLevel b -> a = b.
Proof.
intros a b Ha Hb Hab.
 unfold CLevel in *.
 case_eq (lt_dec a nbLevel );intros g Ha'.
 + rewrite Ha' in Hab.
   case_eq (lt_dec b nbLevel);intros p Hb'.
   - rewrite Hb' in Hab.
     inversion Hab. intuition.
   - omega.
 + omega.
Qed.

Lemma level_gt :
forall x x0, x - x0 < nbLevel ->  CLevel (x - x0) > 0 -> x > x0.
Proof.
intros.
unfold CLevel in *.
case_eq (lt_dec (x - x0) nbLevel ).
intros. rewrite H1 in H0.
simpl in *. omega.
intros. contradict H1. omega.
Qed.

Lemma getNbLevelLe :
forall nbL,
Some nbL = getNbLevel ->
nbL <= CLevel (nbLevel - 1).
Proof.
intros.
unfold getNbLevel in *.
destruct (gt_dec nbLevel 0).
inversion H.
unfold CLevel.
case_eq (lt_dec (nbLevel - 1) nbLevel); intros.
simpl.
omega.
omega.
assert (0 < nbLevel) by apply nbLevelNotZero.
omega.
Qed.

Lemma getNbLevelEq :
forall nbL,
Some nbL = getNbLevel ->
nbL = CLevel (nbLevel - 1).
Proof.
intros.
unfold getNbLevel in *.
destruct (gt_dec nbLevel 0).
inversion H.
destruct nbL.
simpl in *.

unfold CLevel.
case_eq (lt_dec (nbLevel - 1) nbLevel); intros.
inversion H.
subst.
f_equal.
auto.
assert (0 < nbLevel) by apply nbLevelNotZero.
omega.
Qed.

Lemma nbLevelEq :
nbLevel - 1 = CLevel (nbLevel - 1).
Proof.
unfold CLevel.
case_eq(lt_dec (nbLevel - 1) nbLevel); intros.
simpl;trivial.
assert(0<nbLevel) by apply nbLevelNotZero.
omega.
Qed.

Lemma fstLevelLe :
forall l: level ,
fstLevel <= l.
Proof.
unfold fstLevel.
unfold CLevel.
intros.
case_eq( lt_dec 0 nbLevel);intros.
simpl;omega.
assert(0 <nbLevel) by apply nbLevelNotZero.
omega.
Qed.

Lemma getNbLevelLt nbL:
getNbLevel = Some nbL -> nbL < nbLevel.
Proof.
intros.
unfold  getNbLevel in *.
destruct (gt_dec nbLevel 0).
inversion H.
destruct CLevel.
simpl;trivial.
now contradict H.
Qed.

Lemma notFstLevel (level1 : level) :
 0 < level1 ->
Level.eqb level1 fstLevel = false.
Proof.
unfold Level.eqb.
intros.
apply NPeano.Nat.eqb_neq.
unfold fstLevel.
unfold CLevel.
case_eq (lt_dec 0 nbLevel);intros.
simpl.
omega.
assert(0<nbLevel) by apply nbLevelNotZero.
omega.
Qed.

(**** ADT : page **)
Lemma isDefaultPageFalse : forall p,   (defaultPage =? pa p) = false -> pa p <> defaultPage .
Proof.
intros.
apply beq_nat_false in H.
unfold not. intros.
contradict H. symmetry.
unfold defaultPage in *.
unfold CPage in *.
case_eq (lt_dec 0 nbPage).
intros.
rewrite H in H0.
rewrite H0. trivial.
intros.
rewrite H in H0. rewrite H0. intuition.
Qed.

Lemma isDefaultPageTrue : forall p,   (defaultPage =? pa p) = true -> pa p = defaultPage .
Proof.
intros.
apply beq_nat_true in H. symmetry.
unfold defaultPage in *.
unfold CPage in *.
case_eq (lt_dec 0 nbPage).
intros.
rewrite H0 in H.
symmetry.
simpl in *.
destruct p.
simpl in *.
subst.
destruct pa.
simpl in *.
subst.
assert (Hp = Pip_state.CPage_obligation_1 0 l ).
apply proof_irrelevance.
subst.
intuition.
intros.
rewrite H0 in H.
subst.
simpl in *.
destruct p.
simpl in *.
subst.
destruct pa.
simpl in *.
subst.
destruct page_d.
simpl in *.
assert (Hp = Hp0).
apply proof_irrelevance.
subst.
intuition.
Qed.

Lemma pageDecOrNot :
forall p1 p2 : page, p1 = p2 \/ p1<>p2.
Proof.
destruct p1;simpl in *;subst;destruct p2;simpl in *;subst.
assert (Heq :p=p0 \/ p<> p0) by omega.
destruct Heq as [Heq|Heq].
subst.
left;f_equal;apply proof_irrelevance.
right. unfold not;intros.
inversion H.
subst.
now contradict Heq.
Qed.

(** ADT : index **)
Lemma indexEqFalse :
forall a b : nat , a < tableSize -> b < tableSize -> a <> b -> CIndex a <> CIndex b.
Proof.
intros.
unfold CIndex.
case_eq (lt_dec a tableSize).
+ intros.
  case_eq (lt_dec b tableSize).
  - intros.
    unfold not in *.
    intros.
    apply H1.
    inversion H4.
    intuition.
  - intros. contradict H0. assumption.
+ intros. contradict H. intuition.
Qed.

Lemma indexltbTrue :
forall i1 i2 : index ,
Index.ltb i1 i2 = true -> i1 < i2.
Proof. intros. unfold Index.ltb in H.
apply NPeano.Nat.ltb_lt in H.
assumption.
Qed.

Lemma indexltbFalse :
forall i1 i2 : index ,
Index.ltb i1 i2 = false -> i1 >= i2.
Proof.
intros.
unfold Index.ltb in *.
apply not_lt.
apply NPeano.Nat.ltb_nlt in H.
omega.
Qed.

Lemma indexBoundEq :
forall i : index , i>= CIndex (tableSize - 1) -> i =  CIndex (tableSize - 1).
Proof.
intros.
unfold CIndex in *.
destruct (lt_dec (tableSize - 1) tableSize).
simpl in *.
destruct i.
simpl in *.
subst.
assert(i = tableSize - 1). omega.
subst.
assert (Hi = Pip_state.CIndex_obligation_1 (tableSize - 1) l ).
apply proof_irrelevance.
subst. trivial.
contradict n.
assert (0 < tableSize).
assert (tableSize > tableSizeLowerBound).
apply tableSizeBigEnough.
unfold  tableSizeLowerBound in * . omega. omega.
Qed.

Lemma indexDiffLtb :
forall i1 i2 : index, i2 < i1 \/ i1 < i2 <-> i2 <> i1.
Proof.
intros.
split;destruct i1, i2;
simpl in *.
 unfold not;
intros;
inversion H0; omega.
intros.
apply nat_total_order.
unfold not in *; intros; subst.
apply H; f_equal.
apply proof_irrelevance.
Qed.

Lemma indexEqId :
forall i : index, CIndex i = i.
Proof.
intros.
unfold CIndex.
destruct i.
simpl.
case_eq(lt_dec i tableSize); intros.
assert(Pip_state.CIndex_obligation_1 i l = Hi) by apply proof_irrelevance.
subst. reflexivity.
now contradict Hi.
Qed.

Lemma indexMaxEqFalseLt :
forall idx : index, idx <> CIndex (tableSize - 1) -> idx < tableSize - 1.
Proof.
intros.
unfold CIndex in *.
case_eq (lt_dec (tableSize - 1) tableSize).
intros .
rewrite H0 in *.
destruct idx.
simpl in *.
apply not_ge.
unfold not.
intros.
contradict H.
assert (i = tableSize - 1).
omega.
subst.
f_equal.
apply proof_irrelevance.
intros.
assert(tableSizeLowerBound < tableSize) by apply tableSizeBigEnough.
omega.
Qed.

Lemma indexMaxEqFalseLt1 :
forall idx : index, idx <> CIndex (tableSize - 1) -> idx < CIndex (tableSize - 1).
Proof.
intros.
unfold CIndex in *.
case_eq (lt_dec (tableSize - 1) tableSize).
intros .
rewrite H0 in *.
destruct idx.
simpl in *.
apply not_ge.
unfold not.
intros.
contradict H.
assert (i = tableSize - 1).
omega.
subst.
f_equal.
apply proof_irrelevance.
intros.
assert(tableSizeLowerBound < tableSize) by apply tableSizeBigEnough.
omega.
Qed.

Lemma noteqIndex a b:
a < tableSizeLowerBound -> b < tableSizeLowerBound -> a<>b ->
CIndex a <> CIndex b.
Proof.
intros.
apply indexEqFalse;
assert (tableSize > tableSizeLowerBound).
apply tableSizeBigEnough.
unfold tableSizeLowerBound in *.
omega.  apply tableSizeBigEnough.
unfold tableSizeLowerBound in *.
omega. apply tableSizeBigEnough. omega.
Qed.

Lemma indexEqbTrue :
forall idx1 idx2 : index, true = Index.eqb idx1 idx2 ->
idx1 = idx2.
Proof.
unfold Index.eqb in *.
intros.
symmetry in H.
apply beq_nat_true in H.
destruct idx1; destruct idx2.
simpl in *.
subst.
f_equal.
apply proof_irrelevance.
Qed.

Lemma indexLtZero :
forall idx : index, idx < CIndex 0 -> False.
Proof.
intros.
unfold CIndex in *.
case_eq (lt_dec 0 tableSize); intros; rewrite H0 in *.
destruct idx. simpl in *.
omega.
assert (tableSizeLowerBound < tableSize) by apply tableSizeBigEnough.
omega.
Qed.

Lemma indexSEqbZeroOdd :
forall curidx idxsucc,
true = Index.eqb curidx (CIndex 0) ->
succIndexInternal curidx = Some idxsucc ->
Nat.Odd idxsucc.
Proof.
intros.
apply indexEqbTrue in H.
subst.
unfold succIndexInternal in *.
unfold CIndex in H0.
case_eq (lt_dec 0 tableSize); intros; rewrite H in *.
simpl in *.
rewrite H in H0.
inversion H0.
case_eq (lt_dec 1 tableSize).
intros.
simpl.
unfold Nat.Odd.
exists 0.
reflexivity.
intros.
subst.
assert (tableSizeLowerBound < tableSize) by apply tableSizeBigEnough.
unfold tableSizeLowerBound in *.
omega.
assert (tableSizeLowerBound < tableSize) by apply tableSizeBigEnough.
unfold tableSizeLowerBound in *.
omega.
Qed.

Lemma indexZeroNotOdd :
forall idx idxsucc : index,
idx < idxsucc ->
succIndexInternal (CIndex 0) = Some idxsucc ->
~ Nat.Odd idx.
Proof.
intros.
unfold succIndexInternal in *.
unfold CIndex in H0.
case_eq (lt_dec 0 tableSize).
intros.
rewrite H1 in H0.
rewrite H1 in H0.
inversion H0.
case_eq (lt_dec 1 tableSize).
intros.
rewrite H2 in H3.
destruct idxsucc.
inversion H3.
subst.
clear H0 H3.
simpl in *.
inversion H.
rewrite H3.
unfold Nat.Odd.
simpl.
unfold not.
intros.
inversion H0.
omega.
omega.
intros.
assert (tableSizeLowerBound < tableSize) by apply tableSizeBigEnough.
unfold tableSizeLowerBound in *.
omega.
intros.
assert (tableSizeLowerBound < tableSize) by apply tableSizeBigEnough.
unfold tableSizeLowerBound in *.
omega.
Qed.

 Lemma indexSEqbZeroLt :
forall  idxsucc idx : index,
succIndexInternal (CIndex 0)  = Some idxsucc ->
idx < idxsucc ->
idx = CIndex 0.
Proof.
intros.
unfold succIndexInternal in *.
unfold CIndex in H.
case_eq (lt_dec 0 tableSize); intros.
rewrite H1 in H.
rewrite H1 in H.
simpl in *.
inversion H.
case_eq (lt_dec 1 tableSize); intros.
rewrite H2 in H3.
destruct idxsucc.
inversion H3.
simpl in *.
subst.
inversion H0.
unfold CIndex.
case_eq (lt_dec idx tableSize); intros.
destruct idx.
simpl.
f_equal.
apply proof_irrelevance.
omega.
omega.
rewrite H2 in H3.
assert (tableSizeLowerBound < tableSize) by apply tableSizeBigEnough.
unfold tableSizeLowerBound in H4.
omega.
assert (tableSizeLowerBound < tableSize) by apply tableSizeBigEnough.
unfold tableSizeLowerBound in H2.
omega.
Qed.

(*
Lemma indexSuccGt :
Lemma indexSuccGt :
forall idx curidx iIndex : index,
StateLib.Index.succ curidx = Some iIndex ->
idx < curidx ->
idx <> iIndex.
Proof.
intros.
unfold Index.succ in *.
case_eq (lt_dec(curidx + 1) tableSize); intros; rewrite H1 in *.
simpl in *.
destruct idx.
simpl in *.
destruct iIndex.
inversion H.
unfold not; intros.
inversion H2.
subst.
omega.
now contradict H.
Qed.

Lemma indexSuccEqFalse:
forall  curidx iIndex : index,
StateLib.Index.succ curidx = Some iIndex ->
 curidx <> iIndex.
Proof.
intros.
unfold Index.succ in *.
case_eq (lt_dec(curidx + 1) tableSize); intros; rewrite H0 in *.
simpl in *.
destruct iIndex.
inversion H.
subst.
clear H.
unfold not; intros.
destruct curidx.
simpl in *.
inversion H.
omega.
now contradict H.
Qed.

Lemma indexSuccEqFalse:
forall  curidx iIndex : index,
succIndexInternal curidx = Some iIndex ->
 curidx <> iIndex.
Proof.
intros.
unfold succIndexInternal in *.
case_eq (lt_dec(curidx + 1) tableSize); intros; rewrite H0 in *.
simpl in *.
destruct iIndex.
inversion H.
subst.
clear H.
unfold not; intros.
destruct curidx.
simpl in *.
inversion H.
omega.
now contradict H.
Qed.

Lemma indexSuccSuccOddOr (curidx iIndex nextidx idx : index):
succIndexInternal curidx = Some iIndex ->
succIndexInternal iIndex = Some nextidx ->
Nat.Odd curidx ->
Nat.Odd idx ->
idx < nextidx ->
idx = curidx \/ idx < curidx.
Proof.
intros.
unfold succIndexInternal in *.
      destruct (lt_dec (curidx + 1) tableSize); try now contradict H.
      inversion H; clear H.
      destruct (lt_dec (iIndex + 1) tableSize); try now contradict H0.
      inversion H0; clear H0.
      destruct nextidx.
      inversion H4; clear H4.
      destruct iIndex.
      simpl in *.
      subst.
      inversion H5; clear H5.
      destruct curidx.
      simpl in *.
      destruct idx.
      simpl in *.
      rewrite <- H0 in H3.
      clear H0 Hi l0 l Hi0 .
      assert (i1 = i \/ i1 < i).
      unfold Nat.Odd in *.
      destruct H1 ; destruct H2.

      omega.
      destruct H.
      left.
      subst.
      f_equal.
      apply proof_irrelevance.
      right; trivial.
Qed.

Lemma indexSuccSuccEvenOr (curidx iIndex nextidx idx : index):
succIndexInternal curidx = Some iIndex ->
succIndexInternal iIndex = Some nextidx ->
Nat.Even curidx ->
Nat.Even idx ->
idx < nextidx ->
idx = curidx \/ idx < curidx.
Proof.
intros.
unfold succIndexInternal in *.
      destruct (lt_dec (curidx + 1) tableSize); try now contradict H.
      inversion H; clear H.
      destruct (lt_dec (iIndex + 1) tableSize); try now contradict H0.
      inversion H0; clear H0.
      destruct nextidx.
      inversion H4; clear H4.
      destruct iIndex.
      simpl in *.
      subst.
      inversion H5; clear H5.
      destruct curidx.
      simpl in *.
      destruct idx.
      simpl in *.
      rewrite <- H0 in H3.
      clear H0 Hi l0 l Hi0 .
      assert (i1 = i \/ i1 < i).
      destruct H1 ; destruct H2.
      omega.
      destruct H.
      left.
      subst.
      f_equal.
      apply proof_irrelevance.
      right; trivial.
Qed.

Lemma indexSuccSuccEvenOddLt (curidx iIndex nextidx idx : index):
succIndexInternal curidx = Some iIndex ->
succIndexInternal iIndex = Some nextidx ->
Nat.Even idx ->
Nat.Odd curidx ->
idx < nextidx ->
idx < iIndex ->
idx < curidx.
Proof.
intros.
unfold succIndexInternal in *.
      destruct (lt_dec (curidx + 1) tableSize); try now contradict H.
      inversion H; clear H.
      destruct (lt_dec (iIndex + 1) tableSize); try now contradict H0.
      inversion H0; clear H0.
      destruct nextidx.
      inversion H5; clear H5.
      destruct iIndex.
      simpl in *.
      subst.
      inversion H6; clear H6.
      destruct curidx.
      simpl in *.
      destruct idx.
      simpl in *.
      destruct H1; destruct H2.
      subst.

      omega.
Qed.

Lemma indexNotEqSuccNotEq (idx1 idx2 : index):
idx1 < tableSize -1 ->
idx2 < tableSize -1 ->
idx1 <> idx2 ->
succIndexInternal idx2 <> succIndexInternal idx1.
Proof.
intros.
unfold succIndexInternal.
case_eq (lt_dec (idx2 + 1) tableSize); intros; try omega.
case_eq (lt_dec (idx1 + 1) tableSize); intros; try omega.
destruct idx1; destruct idx2; simpl in *.
unfold not; intros Hfalse.
inversion Hfalse.
assert (i0 = i) by omega.
subst.
contradict H1.
f_equal.
apply proof_irrelevance.
Qed.

(** ADT : vaddr **)
Lemma lengthVAddrNotZero (va : vaddr) : fstLevel < (length va -1).
Proof.
 unfold fstLevel.  destruct va.
 simpl. rewrite Hva. unfold CLevel. case_eq (lt_dec 0 nbLevel).
 simpl. intros. omega.
 intros. destruct level_d. simpl. omega.
 Qed.

Lemma CLevelMinusEq0 :
forall (a : level) b , CLevel (a -  b) = CLevel 0 ->   a = CLevel b \/ a < b.
Proof.
intros.
unfold CLevel in *.
case_eq (lt_dec (a - b) nbLevel );
intros lab Hab; rewrite Hab in *.
case_eq(lt_dec 0 nbLevel);
intros l0 H0;
rewrite H0 in*.
inversion H.
case_eq (lt_dec b nbLevel);
intros lb Hb.
simpl in *.
apply NPeano.Nat.sub_0_le in H2.
apply le_lt_or_eq in H2.
destruct H2.
right; assumption.
left.
destruct a.
simpl in *.
subst.
assert (Hl =  Pip_state.CLevel_obligation_1 b lb ) by
apply proof_irrelevance.
subst. reflexivity.
right; destruct a; simpl in *; omega.
assert (0 < nbLevel) by apply nbLevelNotZero.
now contradict H1.
destruct a. simpl in *.
omega.
Qed.
*)

(** beqPairs **)
Lemma beqPairsTrue :
forall table1 idx1 table2 idx2 , table1 = table2 /\ idx1 = idx2 <->
beqPairs (table1, idx1) (table2, idx2) beqPage beqIndex = true.
Proof.
intros.
unfold beqPairs.
cbn.
unfold beqPage , beqIndex .
split.
* case_eq (table1 =? table2) ; case_eq(idx1 =? idx2);intuition.
  apply beq_nat_false in H.
  destruct idx1 , idx2. simpl in *. inversion H3. omega.
  apply beq_nat_false in H0.
  destruct table1, table2. simpl in *.
  inversion H2. omega.
  destruct ((false && false)%bool). trivial.
  apply beq_nat_false in H0.
  destruct table1, table2. simpl in *.
  inversion H2. omega.
* intros.
  case_eq (table1 =? table2) ; case_eq(idx1 =? idx2);intuition.
  apply beq_nat_true in H1; trivial.
  destruct table1, table2; simpl in *; subst; f_equal; apply proof_irrelevance.
  destruct idx1 , idx2; simpl in *.
  apply beq_nat_true in H0; subst; f_equal; apply proof_irrelevance.
  apply beq_nat_true in H1; trivial.
  destruct table1, table2; simpl in *; subst; f_equal; apply proof_irrelevance.
  rewrite H0 in H.
  rewrite H1 in H.
  case_eq ((true && false)%bool); intros.
  apply Bool.andb_true_iff in H2.
  now contradict H2.
  rewrite H2 in H; now contradict H.
  rewrite H0 in H.
  rewrite H1 in H.
  case_eq ((false && true)%bool); intros.
  apply Bool.andb_true_iff in H2.
  now contradict H2.
  rewrite H2 in H; now contradict H.
  apply beq_nat_true in H0.
  destruct idx1 , idx2; simpl in *;subst; f_equal; apply proof_irrelevance.
  rewrite H0 in H.
  rewrite H1 in H.
  case_eq ((false && false)%bool); intros.
  apply Bool.andb_true_iff in H2.
  now contradict H2.
  rewrite H2 in H; now contradict H.
  rewrite H0 in H.
  rewrite H1 in H.
  case_eq ((false && false)%bool); intros.
  apply Bool.andb_true_iff in H2.
  now contradict H2.
  rewrite H2 in H; now contradict H.
Qed.

Lemma beqPairsFalse :
forall table1 idx1 table2 idx2 ,
table1 <> table2 \/ idx1 <> idx2 <->
beqPairs (table1, idx1) (table2, idx2) beqPage beqIndex = false.
Proof.
intros.
unfold beqPairs.
cbn.
unfold beqPage , beqIndex .
intuition.
case_eq (table1 =? table2) ; case_eq(idx1 =? idx2);intuition.
contradict H0.
apply beq_nat_true in H1.
destruct table1, table2. simpl in *. subst.
assert (Hp = Hp0).
apply proof_irrelevance. subst. trivial.
assert((idx1 =? idx2) = false).
apply Nat.eqb_neq. unfold not.
intros.
destruct idx1; destruct idx2.
simpl in *.
subst.
apply H0.
f_equal.
apply proof_irrelevance.
rewrite H.
case_eq ((table1 =? table2) && false).
intros.
apply andb_true_iff in H1.
intuition.
trivial.
case_eq (table1 =? table2) ; case_eq(idx1 =? idx2);intuition.
+ rewrite H1 in H.
  rewrite H0 in H.
  intuition.
+ apply beq_nat_false in H0.
  right.
  intros.
  destruct idx1; destruct idx2.
  simpl in *.
  inversion H2.
  subst.
  now contradict H0.
+ apply beq_nat_false in H1.
  left.
  intros.
  destruct table1; destruct table2.
  simpl in *.
  inversion H2.
  subst.
  now contradict H1.
+ apply beq_nat_false in H1.
  left.
  intros.
  destruct table1; destruct table2.
  simpl in *.
  inversion H2.
  subst.
  now contradict H1.
Qed.

 Lemma idxPRsucNotEqidxPPR : PRidx < tableSize - 1 ->
    exists succidx1 : index, succIndexInternal PRidx = Some succidx1 /\ (succidx1 = PPRidx -> False).
    Proof.
    unfold succIndexInternal.
    case_eq (lt_dec (PRidx + 1) tableSize); intros.
    eexists.
    split.
    instantiate (1:= CIndex (PRidx + 1)).
    f_equal.
    unfold CIndex .
    f_equal.
    destruct PRidx.
    case_eq (lt_dec i tableSize); intros.
    f_equal.
    omega.
    unfold CIndex.
    case_eq(lt_dec (PRidx + 1) tableSize ); intros.

    assert(Hi : {| i := PRidx + 1; Hi := Pip_state.CIndex_obligation_1 (PRidx + 1) l0 |} = PPRidx)
    by trivial.
    contradict Hi.
    subst.
    unfold PRidx. unfold PPRidx.
    unfold CIndex at 3.
    case_eq (lt_dec 10 tableSize); intros.
    unfold not; intros Hii.
    inversion Hii as (Hi2).
    unfold CIndex in Hi2.
    case_eq(lt_dec 0 tableSize); intros Hi1 Hi3; rewrite Hi3 in *.
    simpl in *.
    inversion Hii.
    abstract omega.
    abstract omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    abstract omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    abstract omega.
    abstract omega.
    Qed.
     Lemma idxPPRsuccNotEqidxPR : PPRidx < tableSize - 1 ->
    exists succidx2 : index, succIndexInternal PPRidx = Some succidx2 /\ (succidx2 = PRidx -> False).
    Proof.
    unfold succIndexInternal.
    case_eq (lt_dec (PPRidx + 1) tableSize); intros.
    eexists.
    split.
    instantiate (1:= CIndex (PPRidx + 1)).
    destruct PPRidx.
    case_eq (lt_dec i tableSize); intros.
    f_equal.
    omega.
    unfold CIndex.
    case_eq(lt_dec (PPRidx + 1) tableSize ); intros.
    assert(Hi : {| i := PPRidx + 1; Hi := Pip_state.CIndex_obligation_1 (PPRidx + 1) l0 |} = PRidx)
    by trivial.
    contradict Hi.
    subst.
    unfold PPRidx. unfold PRidx.
    unfold CIndex at 3.
    case_eq (lt_dec 0 tableSize); intros.
    unfold not; intros Hii.
    inversion Hii as (Hi2).
    unfold CIndex in Hi2.
    case_eq(lt_dec 10 tableSize); intros Hi1 Hi3; rewrite Hi3 in *.
    simpl in *.
    inversion Hii.
    abstract omega.
    abstract omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    abstract omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    abstract omega.
    abstract omega.
    Qed.

Lemma idxPRidxPPRNotEq : PRidx <> PPRidx.
    Proof.
      unfold PRidx. unfold PPRidx.
      apply indexEqFalse ;
      assert (tableSize > tableSizeLowerBound).
      apply tableSizeBigEnough.
      unfold tableSizeLowerBound in *.
      abstract omega.  apply tableSizeBigEnough.
      unfold tableSizeLowerBound in *.
      abstract omega.
      apply tableSizeBigEnough.
      abstract omega. Qed.

    Lemma idxPPRsuccNotEqidxPD : PPRidx < tableSize - 1 ->
    exists succidx2 : index, succIndexInternal PPRidx = Some succidx2 /\ (succidx2 = PDidx -> False).
    Proof.
    unfold succIndexInternal.
    case_eq (lt_dec (PPRidx + 1) tableSize); intros.
    eexists.
    split.
    instantiate (1:= CIndex (PPRidx + 1)).
    destruct PPRidx.
    case_eq (lt_dec i tableSize); intros.
    f_equal.
    omega.
    unfold CIndex.
    case_eq(lt_dec (PPRidx + 1) tableSize ); intros.

    assert(Hi : {| i := PPRidx + 1; Hi := Pip_state.CIndex_obligation_1 (PPRidx + 1) l0 |} = PDidx)
    by trivial.
    contradict Hi.
    subst.
    unfold PPRidx. unfold PDidx.
    unfold CIndex at 3.
    case_eq (lt_dec 2 tableSize); intros.
    unfold not; intros Hii.
    inversion Hii as (Hi2).
    unfold CIndex in Hi2.
    case_eq(lt_dec 10 tableSize); intros Hi1 Hi3; rewrite Hi3 in *.
    simpl in *.
    inversion Hii.
    abstract omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    abstract omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    abstract omega.
    abstract omega.
    abstract omega.
    Qed.

Lemma idxPPRidxPDNotEq : PPRidx <> PDidx.
    Proof.
      unfold PPRidx. unfold PDidx.
      apply indexEqFalse ;
      assert (tableSize > tableSizeLowerBound).
      apply tableSizeBigEnough.
      unfold tableSizeLowerBound in *.
      abstract omega.  apply tableSizeBigEnough.
      unfold tableSizeLowerBound in *.
      abstract omega. apply tableSizeBigEnough. abstract omega. Qed.
    Lemma idxPDsucNotEqidxPPR :  PDidx < tableSize - 1 ->
    exists succidx1 : index, succIndexInternal PDidx = Some succidx1 /\ (succidx1 = PPRidx -> False).
    Proof.
    unfold succIndexInternal.
    case_eq (lt_dec (PDidx + 1) tableSize); intros.
    eexists.
    split.
    instantiate (1:= CIndex (PDidx + 1)).
    destruct PDidx.
    case_eq (lt_dec i tableSize); intros.
    f_equal.
    omega.
    unfold CIndex.
    case_eq(lt_dec (PDidx + 1) tableSize ); intros.
    assert(Hi : {| i := PDidx + 1; Hi := Pip_state.CIndex_obligation_1 (PDidx + 1) l0 |} = PPRidx)
    by trivial.
    contradict Hi.
    subst.
    unfold PDidx. unfold PPRidx.
    unfold CIndex at 3.
    case_eq (lt_dec 10 tableSize); intros.
    unfold not; intros Hii.
    inversion Hii as (Hi2).
    unfold CIndex in Hi2.
    case_eq(lt_dec 2 tableSize); intros Hi1 Hi3; rewrite Hi3 in *.
    simpl in *.
    inversion Hii.
    abstract omega.
    abstract omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    abstract omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    abstract omega.
    abstract omega.
    Qed.

 Lemma idxPDidxPPRNotEq : PDidx <> PPRidx.
    Proof.
      unfold PRidx. unfold sh3idx.
      apply indexEqFalse ;
      assert (tableSize > tableSizeLowerBound).
      apply tableSizeBigEnough.
      unfold tableSizeLowerBound in *.
      abstract omega.  apply tableSizeBigEnough.
      unfold tableSizeLowerBound in *.
      abstract omega.
      apply tableSizeBigEnough.
      abstract omega. Qed.

 Lemma idxPPRidxSh1NotEq : PPRidx <> sh1idx.
    Proof.
      unfold PPRidx. unfold sh1idx.
      apply indexEqFalse ;
      assert (tableSize > tableSizeLowerBound).
      apply tableSizeBigEnough.
      unfold tableSizeLowerBound in *.
      abstract omega.  apply tableSizeBigEnough.
      unfold tableSizeLowerBound in *.
      abstract omega. apply tableSizeBigEnough. abstract omega. Qed.

    Lemma idxPPRsuccNotEqidxSh1 : PPRidx < tableSize - 1 ->
    exists succidx2 : index, succIndexInternal PPRidx = Some succidx2 /\ (succidx2 = sh1idx -> False).
    Proof.
    unfold succIndexInternal.
    case_eq (lt_dec (PPRidx + 1) tableSize); intros.
    eexists.
    split.
    instantiate (1:= CIndex (PPRidx + 1)).
    destruct PPRidx.
    case_eq (lt_dec i tableSize); intros.
    f_equal.
    omega.
    unfold CIndex.
    case_eq(lt_dec (PPRidx + 1) tableSize ); intros.

    assert(Hi : {| i := PPRidx + 1; Hi := Pip_state.CIndex_obligation_1 (PPRidx + 1) l0 |} = sh1idx)
    by trivial.
    contradict Hi.
    subst.
    unfold PPRidx. unfold sh1idx.
    unfold CIndex at 3.
    case_eq (lt_dec 4 tableSize); intros.
    unfold not; intros Hii.
    inversion Hii as (Hi2).
    unfold CIndex in Hi2.
    case_eq(lt_dec 10 tableSize); intros Hi1 Hi3; rewrite Hi3 in *.
    simpl in *.
    inversion Hii.
    abstract omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    abstract omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    abstract omega.
    abstract omega.
    abstract omega.
    Qed.

    Lemma idxSh1succNotEqidxPPR : sh1idx < tableSize - 1 ->
    exists succidx1 : index, succIndexInternal sh1idx = Some succidx1 /\ (succidx1 = PPRidx -> False).
    Proof.
    unfold succIndexInternal.
    case_eq (lt_dec (sh1idx + 1) tableSize); intros.
    eexists.
    split.
    instantiate (1:= CIndex (sh1idx + 1)).
    destruct sh1idx.
    case_eq (lt_dec i tableSize); intros.
    f_equal.
    omega.
    unfold CIndex.
    case_eq(lt_dec (sh1idx + 1) tableSize ); intros.

    assert(Hi : {| i := sh1idx + 1; Hi := Pip_state.CIndex_obligation_1 (sh1idx + 1) l0 |} = PPRidx)
    by trivial.
    contradict Hi.
    subst.
    unfold sh1idx. unfold PPRidx.
    unfold CIndex at 3.
    case_eq (lt_dec 10 tableSize); intros.
    unfold not; intros Hii.
    inversion Hii as (Hi2).
    unfold CIndex in Hi2.
    case_eq(lt_dec 4 tableSize); intros Hi1 Hi3; rewrite Hi3 in *.
    simpl in *.
    inversion Hii.
    abstract omega.
    abstract omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    abstract omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    abstract omega.
    abstract omega.
    Qed.

Lemma idxSh1idxPPRnotEq : sh1idx <> PPRidx.
    Proof.
      unfold sh1idx. unfold PPRidx.
      apply indexEqFalse ;
      assert (tableSize > tableSizeLowerBound).
      apply tableSizeBigEnough.
      unfold tableSizeLowerBound in *.
      abstract omega.  apply tableSizeBigEnough.
      unfold tableSizeLowerBound in *.
      abstract omega.
      apply tableSizeBigEnough.
      abstract omega. Qed.

(*

    Lemma idxPPRsuccNotEqidxSh2 : PPRidx < tableSize - 1 ->
    exists succidx2 : index, succIndexInternal PPRidx = Some succidx2 /\ (succidx2 = sh2idx -> False).
    Proof.
    unfold succIndexInternal.
    case_eq (lt_dec (PPRidx + 1) tableSize); intros.
    eexists.
    split.
    instantiate (1:= CIndex (PPRidx + 1)).
    destruct sh1idx.
    case_eq (lt_dec i tableSize); intros.
    f_equal.
    omega.
    unfold CIndex.
    f_equal.
    unfold CIndex .
    case_eq (lt_dec(PPRidx + 1) tableSize); intros.
    f_equal.
    apply proof_irrelevance.
    abstract omega.
    unfold CIndex.
    case_eq(lt_dec (PPRidx + 1) tableSize ); intros.
    assert(Hi : {| i := PPRidx + 1; Hi := Pip_state.CIndex_obligation_1 (PPRidx + 1) l0 |} = sh2idx)
    by trivial.
    contradict Hi.
    subst.
    unfold PPRidx. unfold sh2idx.
    unfold CIndex at 3.
    case_eq (lt_dec 6 tableSize); intros.
    unfold not; intros Hii.
    inversion Hii as (Hi2).
    unfold CIndex in Hi2.
    case_eq(lt_dec 10 tableSize); intros Hi1 Hi3; rewrite Hi3 in *.
    simpl in *.
    inversion Hii.
    abstract omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    abstract omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    abstract omega.
    abstract omega.
    abstract omega.
    Qed.

Lemma idxPPRidxSh2NotEq : PPRidx <> sh2idx. Proof.
      unfold PPRidx. unfold sh2idx.
      apply indexEqFalse ;
      assert (tableSize > tableSizeLowerBound).
      apply tableSizeBigEnough.
      unfold tableSizeLowerBound in *.
      abstract omega.  apply tableSizeBigEnough.
      unfold tableSizeLowerBound in *.
      abstract omega.
      apply tableSizeBigEnough.
      abstract omega. Qed.
    Lemma idxSh2succNotEqidxPPR : sh2idx < tableSize - 1 ->
    exists succidx1 : index, succIndexInternal sh2idx = Some succidx1 /\ (succidx1 = PPRidx -> False).
    Proof.
    unfold succIndexInternal.
    case_eq (lt_dec (sh2idx + 1) tableSize); intros.
    eexists.
    split.
    instantiate (1:= CIndex (sh2idx + 1)).
    destruct sh2idx.
    case_eq (lt_dec i tableSize); intros.
    f_equal.
    omega.
    unfold CIndex.
    case_eq (lt_dec(sh2idx + 1) tableSize); intros.
    contradict H2.
    subst.
    unfold sh2idx. unfold PPRidx.
    unfold CIndex at 3.
    case_eq (lt_dec 10 tableSize); intros.
    unfold not; intros Hii.
    inversion Hii as (Hi2).
    unfold CIndex in Hi2.
    case_eq(lt_dec 6 tableSize); intros Hi1 Hi3; rewrite Hi3 in *.
    simpl in *.
    inversion Hii.
    abstract omega.
    abstract omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    abstract omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    abstract omega.
    abstract omega.
    Qed.

Lemma idxSh2idxPPRnotEq : sh2idx <> PPRidx.
    Proof.
      unfold sh1idx. unfold sh3idx.
      apply indexEqFalse ;
      assert (tableSize > tableSizeLowerBound).
      apply tableSizeBigEnough.
      unfold tableSizeLowerBound in *.
      abstract omega.  apply tableSizeBigEnough.
      unfold tableSizeLowerBound in *.
      abstract omega.
      apply tableSizeBigEnough.
      abstract omega. Qed.

    Lemma idxPPRsuccNotEqidxSh3 : PPRidx < tableSize - 1 ->
    exists succidx2 : index, succIndexInternal PPRidx = Some succidx2 /\ (succidx2 = sh3idx -> False).
    Proof.
    unfold succIndexInternal.
    case_eq (lt_dec (PPRidx + 1) tableSize); intros.
    eexists.
    split.
    instantiate (1:= CIndex (PPRidx + 1)).
    f_equal.
    unfold CIndex .
    case_eq (lt_dec(PPRidx + 1) tableSize); intros.
    f_equal.
    apply proof_irrelevance.
    abstract omega.
    unfold CIndex.
    case_eq(lt_dec (PPRidx + 1) tableSize ); intros.

     assert(Hi : {| i := PPRidx + 1; Hi := Pip_state.CIndex_obligation_1 (PPRidx + 1) l0 |} = sh3idx)
    by trivial.
    contradict Hi.
    subst.
    unfold PPRidx. unfold sh3idx.
    unfold CIndex at 3.
    case_eq (lt_dec 8 tableSize); intros.
    unfold not; intros Hii.
    inversion Hii as (Hi2).
    unfold CIndex in Hi2.
    case_eq(lt_dec 10 tableSize); intros Hi1 Hi3; rewrite Hi3 in *.
    simpl in *.
    inversion Hii.
    abstract omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    abstract omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    abstract omega.
    abstract omega.
    abstract omega.
    Qed.

    Lemma idxSh3succNotEqPPRidx : sh3idx < tableSize - 1 ->
    exists succidx1 : index, succIndexInternal sh3idx = Some succidx1 /\ (succidx1 = PPRidx -> False).
    Proof.
    unfold succIndexInternal.
    case_eq (lt_dec (sh3idx + 1) tableSize); intros.
    eexists.
    split.
    instantiate (1:= CIndex (sh3idx + 1)).
    f_equal.
    unfold CIndex .
    case_eq (lt_dec(sh3idx + 1) tableSize); intros.
    f_equal.
    apply proof_irrelevance.
    abstract omega.
    unfold CIndex.
    case_eq(lt_dec (sh3idx + 1) tableSize ); intros.
     assert(Hi : {| i := sh3idx + 1; Hi := Pip_state.CIndex_obligation_1 (sh3idx + 1) l0 |} = PPRidx)
    by trivial.
    contradict Hi.
    subst.
    unfold sh3idx. unfold PPRidx.
    unfold CIndex at 3.
    case_eq (lt_dec 10 tableSize); intros.
    unfold not; intros Hii.
    inversion Hii as (Hi2).
    unfold CIndex in Hi2.
    case_eq(lt_dec 8 tableSize); intros Hi1 Hi3; rewrite Hi3 in *.
    simpl in *.
    inversion Hii.
    abstract omega.
    abstract omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    abstract omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    abstract omega.
    abstract omega.
    Qed.

 Lemma idxPPRidxSh3NotEq : PPRidx <> sh3idx.
    Proof.
      unfold PPRidx. unfold sh3idx.
      apply indexEqFalse ;
      assert (tableSize > tableSizeLowerBound).
      apply tableSizeBigEnough.
      unfold tableSizeLowerBound in *.
      abstract omega.  apply tableSizeBigEnough.
      unfold tableSizeLowerBound in *.
      abstract omega.
       apply tableSizeBigEnough. abstract omega. Qed.

    Lemma idxSh3succNotEqPRidx : sh3idx < tableSize - 1 ->
    exists succidx2 : index, succIndexInternal sh3idx = Some succidx2 /\ (succidx2 = PRidx -> False).
    Proof.
    unfold succIndexInternal.
    case_eq (lt_dec (sh3idx + 1) tableSize); intros.
    eexists.
    split.
    instantiate (1:= CIndex (sh3idx + 1)).
    f_equal.
    unfold CIndex .
    case_eq (lt_dec(sh3idx + 1) tableSize); intros.
    f_equal.
    apply proof_irrelevance.
    abstract omega.
    unfold CIndex.
    case_eq(lt_dec (sh3idx + 1) tableSize ); intros.

     assert(Hi : {| i := sh3idx + 1; Hi := Pip_state.CIndex_obligation_1 (sh3idx + 1) l0 |} = PRidx)
    by trivial.
    contradict Hi.
    subst.
    unfold sh3idx. unfold PRidx.
    unfold CIndex at 3.
    case_eq (lt_dec 0 tableSize); intros.
    unfold not; intros Hii.
    inversion Hii as (Hi2).
    unfold CIndex in Hi2.
    case_eq(lt_dec 8 tableSize); intros Hi1 Hi3; rewrite Hi3 in *.
    simpl in *.
    inversion Hii.
    abstract omega.
    abstract omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    abstract omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    abstract omega.
    abstract omega.
    Qed.

    Lemma idxPRsuccNotEqidxSh3 : PRidx < tableSize - 1 -> exists succidx1 : index, succIndexInternal PRidx = Some succidx1 /\ (succidx1 = sh3idx -> False).
    Proof.
    unfold succIndexInternal.
    case_eq (lt_dec (PRidx + 1) tableSize); intros.
    eexists.
    split.
    instantiate (1:= CIndex (PRidx + 1)).
    f_equal.
    unfold CIndex .
    case_eq (lt_dec(PRidx + 1) tableSize); intros.
    f_equal.
    apply proof_irrelevance.
    abstract omega.
    unfold CIndex.
    case_eq(lt_dec (PRidx + 1) tableSize ); intros.
    assert(Hi : {| i := PRidx + 1; Hi := Pip_state.CIndex_obligation_1 (PRidx + 1) l0 |} = sh3idx)
    by trivial.
    contradict Hi.
    subst.
    unfold sh3idx. unfold PRidx.
    unfold CIndex at 3.
    case_eq (lt_dec 8 tableSize); intros.
    unfold not; intros Hii.
    inversion Hii as (Hi2).
    unfold CIndex in Hi2.
    case_eq(lt_dec 0 tableSize); intros Hi1 Hi3; rewrite Hi3 in *.
    simpl in *.
    inversion Hii.
    abstract omega.
    abstract omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    abstract omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    abstract omega.
    abstract omega.
    Qed.

    Lemma  idxPRidxSh3NotEq : PRidx <> sh3idx.
    Proof.
    (* *)
      unfold PRidx. unfold sh3idx.
      apply indexEqFalse ;
      assert (tableSize > tableSizeLowerBound).
      apply tableSizeBigEnough.
      unfold tableSizeLowerBound in *.
      abstract omega.  apply tableSizeBigEnough.
      unfold tableSizeLowerBound in *.
      abstract omega. apply tableSizeBigEnough. abstract omega. Qed.

    Lemma idxSh3succNotEqidxPDidx : sh3idx < tableSize - 1 ->
    exists succidx2 : index, succIndexInternal sh3idx = Some succidx2 /\ (succidx2 = PDidx -> False).
    Proof.
    unfold succIndexInternal.
    case_eq (lt_dec (sh3idx + 1) tableSize); intros.
    eexists.
    split.
    instantiate (1:= CIndex (sh3idx + 1)).
    f_equal.
    unfold CIndex .
    case_eq (lt_dec(sh3idx + 1) tableSize); intros.
    f_equal.
    apply proof_irrelevance.
    abstract omega.
    unfold CIndex.
    case_eq(lt_dec (sh3idx + 1) tableSize ); intros.
     assert(Hi : {| i := sh3idx + 1; Hi := Pip_state.CIndex_obligation_1 (sh3idx + 1) l0 |} = PDidx)
    by trivial.
    contradict Hi.
    subst.
    unfold PDidx. unfold sh3idx.
    unfold CIndex at 3.
    case_eq (lt_dec 2 tableSize); intros.
    unfold not; intros Hii.
    inversion Hii as (Hi2).
    unfold CIndex in Hi2.
    case_eq(lt_dec 8 tableSize); intros Hi1 Hi3; rewrite Hi3 in *.
    simpl in *.
    inversion Hii.
    abstract omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    abstract omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    abstract omega.
    abstract omega.
    abstract omega.
    Qed.

    Lemma idxPDsucNotEqidxSh3 : PDidx < tableSize - 1 ->
    exists succidx1 : index, succIndexInternal PDidx = Some succidx1 /\ (succidx1 = sh3idx -> False).
    Proof.
    unfold succIndexInternal.
    case_eq (lt_dec (PDidx + 1) tableSize); intros.
    eexists.
    split.
    instantiate (1:= CIndex (PDidx + 1)).
    f_equal.
    unfold CIndex .
    case_eq (lt_dec(PDidx + 1) tableSize); intros.
    f_equal.
    apply proof_irrelevance.
    abstract omega.
    unfold CIndex.
    case_eq(lt_dec (PDidx + 1) tableSize ); intros.

     assert(Hi : {| i := PDidx + 1; Hi := Pip_state.CIndex_obligation_1 (PDidx + 1) l0 |} = sh3idx)
    by trivial.
    contradict Hi.
    subst.
    unfold sh3idx. unfold PDidx.
    unfold CIndex at 3.
    case_eq (lt_dec 8 tableSize); intros.
    unfold not; intros Hii.
    inversion Hii as (Hi2).
    unfold CIndex in Hi2.
    case_eq(lt_dec 2 tableSize); intros Hi1 Hi3; rewrite Hi3 in *.
    simpl in *.
    inversion Hii.
    abstract omega.
    abstract omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    abstract omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    abstract omega.
    abstract omega.
    Qed.

    Lemma idxPDidxSh3notEq : PDidx <> sh3idx.
    Proof.
(*
 *)      unfold PDidx. unfold sh3idx.
      apply indexEqFalse ;
      assert (tableSize > tableSizeLowerBound).
      apply tableSizeBigEnough.
      unfold tableSizeLowerBound in *.
      abstract omega.  apply tableSizeBigEnough.
      unfold tableSizeLowerBound in *.
      abstract omega. apply tableSizeBigEnough. abstract omega.
      Qed.

    Lemma idxSh3succNotEqidxSh1 :
    sh3idx < tableSize - 1 ->
     exists succidx2 : index, succIndexInternal sh3idx = Some succidx2 /\ (succidx2 = sh1idx -> False).
     Proof.
    unfold succIndexInternal.
    case_eq (lt_dec (sh3idx + 1) tableSize); intros.
    eexists.
    split.
    instantiate (1:= CIndex (sh3idx + 1)).
    f_equal.
    unfold CIndex .
    case_eq (lt_dec(sh3idx + 1) tableSize); intros.
    f_equal.
    apply proof_irrelevance.
    omega.
    unfold CIndex.
    case_eq(lt_dec (sh3idx + 1) tableSize ); intros.

     assert(Hi : {| i := sh3idx + 1; Hi := Pip_state.CIndex_obligation_1 (sh3idx + 1) l0 |} = sh1idx)
    by trivial.
    contradict Hi.
    subst.
    unfold sh3idx. unfold sh1idx.
    unfold CIndex at 3.
    case_eq (lt_dec 4 tableSize); intros.
    unfold not; intros Hii.
    inversion Hii as (Hi2).
    unfold CIndex in Hi2.
    case_eq(lt_dec 8 tableSize); intros Hi1 Hi3; rewrite Hi3 in *.
    simpl in *.
    inversion Hii.
    omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    omega.
    omega.
    omega.
    Qed.
    Lemma sh1idxSh3idxNotEq : sh1idx < tableSize - 1 ->
    exists succidx1 : index, succIndexInternal sh1idx = Some succidx1 /\ (succidx1 = sh3idx -> False).
    Proof.
    unfold succIndexInternal.
    case_eq (lt_dec (sh1idx + 1) tableSize); intros.
    eexists.
    split.
    instantiate (1:= CIndex (sh1idx + 1)).
    f_equal.
    unfold CIndex .
    case_eq (lt_dec(sh1idx + 1) tableSize); intros.
    f_equal.
    apply proof_irrelevance.
    omega.
    unfold CIndex.
    case_eq(lt_dec (sh1idx + 1) tableSize ); intros.

     assert(Hi : {| i := sh1idx + 1; Hi := Pip_state.CIndex_obligation_1 (sh1idx + 1) l0 |} = sh3idx)
    by trivial.
    contradict Hi.
    subst.
    unfold sh1idx. unfold sh3idx.
    unfold CIndex at 3.
    case_eq (lt_dec 8 tableSize); intros.
    unfold not; intros Hii.
    inversion Hii as (Hi2).
    unfold CIndex in Hi2.
    case_eq(lt_dec 4 tableSize); intros Hi1 Hi3; rewrite Hi3 in *.
    simpl in *.
    inversion Hii.
    omega.
    omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    omega.
    omega.
    Qed.
    Lemma idxSh1idxSh3notEq :  sh1idx <> sh3idx.
     Proof.
      unfold sh1idx. unfold sh3idx.
      apply indexEqFalse ;
      assert (tableSize > tableSizeLowerBound).
      apply tableSizeBigEnough.
      unfold tableSizeLowerBound in *.
      omega.  apply tableSizeBigEnough.
      unfold tableSizeLowerBound in *.
      omega. apply tableSizeBigEnough. omega.
      Qed.

    Lemma idxSh3succNotEqidxSh2 : sh3idx < tableSize - 1 ->
    exists succidx2 : index, succIndexInternal sh3idx = Some succidx2 /\ (succidx2 = sh2idx -> False).
    Proof.
    unfold succIndexInternal.
    case_eq (lt_dec (sh3idx + 1) tableSize); intros.
    eexists.
    split.
    instantiate (1:= CIndex (sh3idx + 1)).
    f_equal.
    unfold CIndex .
    case_eq (lt_dec(sh3idx + 1) tableSize); intros.
    f_equal.
    apply proof_irrelevance.
    omega.
    unfold CIndex.
    case_eq(lt_dec (sh3idx + 1) tableSize ); intros.
    assert(Hi : {| i := sh3idx + 1; Hi := Pip_state.CIndex_obligation_1 (sh3idx + 1) l0 |} = sh2idx)
    by trivial.
    contradict Hi.
    subst.
    unfold sh3idx. unfold sh2idx.
    unfold CIndex at 3.
    case_eq (lt_dec 6 tableSize); intros.
    unfold not; intros Hii.
    inversion Hii as (Hi2).
    unfold CIndex in Hi2.
    case_eq(lt_dec 8 tableSize); intros Hi1 Hi3; rewrite Hi3 in *.
    simpl in *.
    inversion Hii.
    omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    omega.
    omega.
    omega.
    Qed.

    Lemma idxSh2succNotEqidxSh3 : sh2idx < tableSize - 1 ->
    exists succidx1 : index, succIndexInternal sh2idx = Some succidx1 /\ (succidx1 = sh3idx -> False).
    Proof.
    unfold succIndexInternal.
    case_eq (lt_dec (sh2idx + 1) tableSize); intros.
    eexists.
    split.
    instantiate (1:= CIndex (sh2idx + 1)).
    f_equal.
    unfold CIndex .
    case_eq (lt_dec(sh2idx + 1) tableSize); intros.
    f_equal.
    apply proof_irrelevance.
    omega.
    unfold CIndex.
    case_eq(lt_dec (sh2idx + 1) tableSize ); intros.
     assert(Hi : {| i := sh2idx + 1; Hi := Pip_state.CIndex_obligation_1 (sh2idx + 1) l0 |} = sh3idx)
    by trivial.
    contradict Hi.
    subst.
    unfold sh3idx. unfold sh2idx.
    unfold CIndex at 3.
    case_eq (lt_dec 8 tableSize); intros.
    unfold not; intros Hii.
    inversion Hii as (Hi2).
    unfold CIndex in Hi2.
    case_eq(lt_dec 6 tableSize); intros Hi1 Hi3; rewrite Hi3 in *.
    simpl in *.
    inversion Hii.
    omega.
    omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    omega.
    omega.
    Qed.

    Lemma idxSh2idxSh3notEq : sh2idx <> sh3idx .
    Proof.
      unfold sh2idx. unfold sh3idx.
      apply indexEqFalse ;
      assert (tableSize > tableSizeLowerBound).
      apply tableSizeBigEnough.
      unfold tableSizeLowerBound in *.
      omega.  apply tableSizeBigEnough.
      unfold tableSizeLowerBound in *.
      omega. apply tableSizeBigEnough. omega.
     Qed.

   Lemma  idxSh2succNotEqidxPR : sh2idx < tableSize - 1 ->
   exists succidx2 : index, succIndexInternal sh2idx = Some succidx2 /\ (succidx2 = PRidx -> False).
   Proof.
    unfold succIndexInternal.
    case_eq (lt_dec (sh2idx + 1) tableSize); intros.
    eexists.
    split.
    instantiate (1:= CIndex (sh2idx + 1)).
    f_equal.
    unfold CIndex .
    case_eq (lt_dec(sh2idx + 1) tableSize); intros.
    f_equal.
    apply proof_irrelevance.
    omega.
    unfold CIndex.
    case_eq(lt_dec (sh2idx + 1) tableSize ); intros.

     assert(Hi : {| i := sh2idx + 1; Hi := Pip_state.CIndex_obligation_1 (sh2idx + 1) l0 |} = PRidx)
    by trivial.
    contradict Hi.
    subst.
    unfold sh2idx. unfold PRidx.
    unfold CIndex at 3.
    case_eq (lt_dec 0 tableSize); intros.
    unfold not; intros Hii.
    inversion Hii as (Hi2).
    unfold CIndex in Hi2.
    case_eq(lt_dec 6 tableSize); intros Hi1 Hi3; rewrite Hi3 in *.
    simpl in *.
    inversion Hii.
    omega.
    omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    omega.
    omega.
    Qed.

        Lemma idxPRsuccNotEqidxSh2 : PRidx < tableSize - 1 ->
    exists succidx1 : index, succIndexInternal PRidx = Some succidx1 /\ (succidx1 = sh2idx -> False).
    Proof.
    unfold succIndexInternal.
    case_eq (lt_dec (PRidx + 1) tableSize); intros.
    eexists.
    split.
    instantiate (1:= CIndex (PRidx + 1)).
    f_equal.
    unfold CIndex .
    case_eq (lt_dec(PRidx + 1) tableSize); intros.
    f_equal.
    apply proof_irrelevance.
    omega.
    unfold CIndex.
    case_eq(lt_dec (PRidx + 1) tableSize ); intros.

     assert(Hi : {| i := PRidx + 1; Hi := Pip_state.CIndex_obligation_1 (PRidx + 1) l0 |} = sh2idx)
    by trivial.
    contradict Hi.
    subst.
    unfold sh2idx. unfold PRidx.
    unfold CIndex at 3.
    case_eq (lt_dec 6 tableSize); intros.
    unfold not; intros Hii.
    inversion Hii as (Hi2).
    unfold CIndex in Hi2.
    case_eq(lt_dec 0 tableSize); intros Hi1 Hi3; rewrite Hi3 in *.
    simpl in *.
    inversion Hii.
    omega.
    omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    omega.
    omega.
    Qed.
        Lemma idxPRidxSh2NotEq : PRidx <> sh2idx.
    Proof.
      unfold PRidx. unfold sh2idx.
      apply indexEqFalse ;
      assert (tableSize > tableSizeLowerBound).
      apply tableSizeBigEnough.
      unfold tableSizeLowerBound in *.
      omega.  apply tableSizeBigEnough.
      unfold tableSizeLowerBound in *.
      omega. apply tableSizeBigEnough. omega.
      Qed.

          Lemma idxSh2succNotEqidxPD : sh2idx < tableSize - 1 ->
     exists succidx2 : index, succIndexInternal sh2idx = Some succidx2 /\ (succidx2 = PDidx -> False).
     Proof.
    unfold succIndexInternal.
    case_eq (lt_dec (sh2idx + 1) tableSize); intros.
    eexists.
    split.
    instantiate (1:= CIndex (sh2idx + 1)).
    f_equal.
    unfold CIndex .
    case_eq (lt_dec(sh2idx + 1) tableSize); intros.
    f_equal.
    apply proof_irrelevance.
    omega.
    unfold CIndex.
    case_eq(lt_dec (sh2idx + 1) tableSize ); intros.
    assert(Hi : {| i := sh2idx + 1; Hi := Pip_state.CIndex_obligation_1 (sh2idx + 1) l0 |} = PDidx)
    by trivial.
    contradict Hi.
    subst.
    unfold sh2idx. unfold PDidx.
    unfold CIndex at 3.
    case_eq (lt_dec 2 tableSize); intros.
    unfold not; intros Hii.
    inversion Hii as (Hi2).
    unfold CIndex in Hi2.
    case_eq(lt_dec 6 tableSize); intros Hi1 Hi3; rewrite Hi3 in *.
    simpl in *.
    inversion Hii.
    omega.

    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    omega.
    omega.

    omega.
    Qed.

        Lemma idxPDsucNotEqidxSh2 :
    PDidx < tableSize - 1 ->
    exists succidx1 : index, succIndexInternal PDidx = Some succidx1 /\ (succidx1 = sh2idx -> False).
    Proof.
    unfold succIndexInternal.
    case_eq (lt_dec (PDidx + 1) tableSize); intros.
    eexists.
    split.
    instantiate (1:= CIndex (PDidx + 1)).
    f_equal.
    unfold CIndex .
    case_eq (lt_dec(PDidx + 1) tableSize); intros.
    f_equal.
    apply proof_irrelevance.
    omega.
    unfold CIndex.
    case_eq(lt_dec (PDidx + 1) tableSize ); intros.

    assert(Hi : {| i := PDidx + 1; Hi := Pip_state.CIndex_obligation_1 (PDidx + 1) l0 |} = sh2idx)
    by trivial.
    contradict Hi.
    subst.
    unfold sh2idx. unfold PDidx.
    unfold CIndex at 3.
    case_eq (lt_dec 6 tableSize); intros.
    unfold not; intros Hii.
    inversion Hii as (Hi2).
    unfold CIndex in Hi2.
    case_eq(lt_dec 2 tableSize); intros Hi1 Hi3; rewrite Hi3 in *.
    simpl in *.
    inversion Hii.
    omega.
    omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    omega.
    omega.
    Qed.

    Lemma idxPDidxSh2notEq : PDidx <> sh2idx .
    Proof.
      unfold PDidx. unfold sh2idx.
      apply indexEqFalse ;
      assert (tableSize > tableSizeLowerBound).
      apply tableSizeBigEnough.
      unfold tableSizeLowerBound in *.
      omega.  apply tableSizeBigEnough.
      unfold tableSizeLowerBound in *.
      omega. apply tableSizeBigEnough. omega. Qed.

          Lemma idxSh2succNotEqidxSh1 :
    sh2idx < tableSize - 1 ->
    exists succidx2 : index, succIndexInternal sh2idx = Some succidx2 /\ (succidx2 = sh1idx -> False).
    Proof.
    unfold succIndexInternal.
    case_eq (lt_dec (sh2idx + 1) tableSize); intros.
    eexists.
    split.
    instantiate (1:= CIndex (sh2idx + 1)).
    f_equal.
    unfold CIndex .
    case_eq (lt_dec(sh2idx + 1) tableSize); intros.
    f_equal.
    apply proof_irrelevance.
    omega.
    unfold CIndex.
    case_eq(lt_dec (sh2idx + 1) tableSize ); intros.
      assert(Hi : {| i := sh2idx + 1; Hi := Pip_state.CIndex_obligation_1 (sh2idx + 1) l0 |} = sh1idx)
    by trivial.
    contradict Hi.
    subst.
    unfold sh1idx. unfold sh2idx.
    unfold CIndex at 3.
    case_eq (lt_dec 4 tableSize); intros.
    unfold not; intros Hii.
    inversion Hii as (Hi2).
    unfold CIndex in Hi2.
    case_eq(lt_dec 6 tableSize); intros Hi1 Hi3; rewrite Hi3 in *.
    simpl in *.
    inversion Hii.
    omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    omega.
    omega.
    omega.
    Qed.

      Lemma idxSh1succNotEqidxSh2 :
    sh1idx < tableSize - 1 ->
    exists succidx1 : index, succIndexInternal sh1idx = Some succidx1 /\ (succidx1 = sh2idx -> False).
    Proof.
    unfold succIndexInternal.
    case_eq (lt_dec (sh1idx + 1) tableSize); intros.
    eexists.
    split.
    instantiate (1:= CIndex (sh1idx + 1)).
    f_equal.
    unfold CIndex .
    case_eq (lt_dec(sh1idx + 1) tableSize); intros.
    f_equal.
    apply proof_irrelevance.
    omega.
    unfold CIndex.
    case_eq(lt_dec (sh1idx + 1) tableSize ); intros.

     assert(Hi : {| i := sh1idx + 1; Hi := Pip_state.CIndex_obligation_1 (sh1idx + 1) l0 |} = sh2idx)
    by trivial.
    contradict Hi.
    subst.
    unfold sh1idx. unfold sh2idx.
    unfold CIndex at 3.
    case_eq (lt_dec 6 tableSize); intros.
    unfold not; intros Hii.
    inversion Hii as (Hi2).
    unfold CIndex in Hi2.
    case_eq(lt_dec 4 tableSize); intros Hi1 Hi3; rewrite Hi3 in *.
    simpl in *.
    inversion Hii.
    omega.
    omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    omega.
    omega.
    Qed.

    Lemma idxSh1succNotEqidxPR :
    sh1idx < tableSize - 1 ->
    exists succidx2 : index, succIndexInternal sh1idx = Some succidx2 /\ (succidx2 = PRidx -> False).
    Proof.
    unfold succIndexInternal.
    case_eq (lt_dec (sh1idx + 1) tableSize); intros.
    eexists.
    split.
    instantiate (1:= CIndex (sh1idx + 1)).
    f_equal.
    unfold CIndex .
    case_eq (lt_dec(sh1idx + 1) tableSize); intros.
    f_equal.
    apply proof_irrelevance.
    omega.
    unfold CIndex.
    case_eq(lt_dec (sh1idx + 1) tableSize ); intros.
    assert(Hi : {| i := sh1idx + 1; Hi := Pip_state.CIndex_obligation_1 (sh1idx + 1) l0 |} = PRidx)
    by trivial.
    contradict Hi.
    subst.
    unfold sh1idx. unfold PRidx.
    unfold CIndex at 3.
    case_eq (lt_dec 4 tableSize); intros.
    unfold not; intros Hii.
    inversion Hii as (Hi2).
    unfold CIndex in Hi2.
    case_eq(lt_dec 0 tableSize); intros Hi1 Hi3; rewrite Hi3 in *.
    simpl in *.
    inversion Hii.
    omega.
    omega.

    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    omega.
    omega.
    Qed.
        Lemma idxPRsuccNotEqidxSh1 :
    PRidx + 1 < tableSize ->
(*     PRidx + 1< tableSize - 1 ->  *)
    exists succidx1 : index, succIndexInternal PRidx = Some succidx1 /\ (succidx1 = sh1idx -> False).
    Proof.
    unfold succIndexInternal.
    case_eq (lt_dec (PRidx + 1) tableSize); intros.
    eexists.
    split.
    instantiate (1:= CIndex (PRidx + 1)).
    f_equal.
    unfold CIndex .
    case_eq (lt_dec(PRidx + 1) tableSize); intros.
    f_equal.
    apply proof_irrelevance.
    omega.
    unfold CIndex.
    case_eq(lt_dec (PRidx + 1) tableSize ); intros.
    assert(Hi : {| i := PRidx + 1; Hi := Pip_state.CIndex_obligation_1 (PRidx + 1) l0 |} = sh1idx)
    by trivial.
    contradict Hi.
    subst.
    unfold sh1idx. unfold PRidx.
    unfold CIndex at 3.
    case_eq (lt_dec 4 tableSize); intros.
    unfold not; intros Hii.
    inversion Hii as (Hi2).
    unfold CIndex in Hi2.
    case_eq(lt_dec 0 tableSize); intros Hi1 Hi3; rewrite Hi3 in *.
    simpl in *.
    inversion Hii.
    omega.
    omega.

    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    omega.
    omega.
    omega.
    Qed.
Lemma idxPRidxSh1NotEq : PRidx <> sh1idx.
    Proof.
      unfold PRidx. unfold sh1idx.
      apply indexEqFalse ;
      assert (tableSize > tableSizeLowerBound).
      apply tableSizeBigEnough.
      unfold tableSizeLowerBound in *.
      omega.  apply tableSizeBigEnough.
      unfold tableSizeLowerBound in *.
      omega. apply tableSizeBigEnough. omega.
      Qed.

          Lemma idxSh1succNotEqidxPD :
    sh1idx + 1 < tableSize ->
    exists succidx2 : index, succIndexInternal sh1idx = Some succidx2 /\ (succidx2 = PDidx -> False).
    Proof.
    unfold succIndexInternal.
    case_eq (lt_dec (sh1idx + 1) tableSize); intros.
    eexists.
    split.
    instantiate (1:= CIndex (sh1idx + 1)).
    f_equal.
    unfold CIndex .
    case_eq (lt_dec(sh1idx + 1) tableSize); intros.
    f_equal.
    apply proof_irrelevance.
    omega.
    unfold CIndex.
    case_eq(lt_dec (sh1idx + 1) tableSize ); intros.
    assert(Hi : {| i := sh1idx + 1; Hi := Pip_state.CIndex_obligation_1 (sh1idx + 1) l0 |} = PDidx)
    by trivial.
    contradict Hi.
    subst.
    unfold sh1idx. unfold PDidx.
    unfold CIndex at 3.
    case_eq (lt_dec 2 tableSize); intros.
    unfold not; intros Hii.
    inversion Hii as (Hi2).
    unfold CIndex in Hi2.
    case_eq(lt_dec 4 tableSize); intros Hi1 Hi3; rewrite Hi3 in *.
    simpl in *.
    inversion Hii.
    omega.
(*     omega.

    contradict H13.
    subst.
    unfold PDidx. unfold sh1idx.
    unfold CIndex at 3.
    case_eq (lt_dec 2 tableSize); intros.
    unfold not; intros.
    inversion H14.
    unfold CIndex in H16.
    case_eq(lt_dec 4 tableSize); intros; rewrite H15 in *.
    inversion H16. *)
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    omega.
    omega.
    omega.
    Qed.

        Lemma  idxPDsucNotEqidxSh1 :
    PDidx + 1 < tableSize ->
    exists succidx1 : index, succIndexInternal PDidx = Some succidx1 /\ (succidx1 = sh1idx -> False).
    Proof.
    unfold succIndexInternal.
    case_eq (lt_dec (PDidx + 1) tableSize); intros.
    eexists.
    split.
    instantiate (1:= CIndex (PDidx + 1)).
    destruct PDidx.
    case_eq (lt_dec i tableSize); intros.
    f_equal.
    omega.
    unfold CIndex.
    case_eq(lt_dec (PDidx + 1) tableSize ); intros.
    assert(Hi : {| i := PDidx + 1; Hi := Pip_state.CIndex_obligation_1 (PDidx + 1) l0 |} = sh1idx)
    by trivial.
    contradict Hi.
    subst.
    unfold sh1idx. unfold PDidx.
    unfold CIndex at 3.
    case_eq (lt_dec 4 tableSize); intros.
    unfold not; intros Hii.
    inversion Hii as (Hi2).
    unfold CIndex in Hi2.
    case_eq(lt_dec 2 tableSize); intros Hi1 Hi3; rewrite Hi3 in *.
    simpl in *.
    inversion Hii.
    omega.
    omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    omega.
    omega.
    Qed.

          Lemma idxPDsucNotEqidxPR :
    PDidx + 1 < tableSize ->
     exists succidx2 : index, succIndexInternal PDidx = Some succidx2 /\ (succidx2 = PRidx -> False).
     Proof.
    unfold succIndexInternal.
    case_eq (lt_dec (PDidx + 1) tableSize); intros.
    eexists.
    split.
    instantiate (1:= CIndex (PDidx + 1)).
    f_equal.
    unfold CIndex .
    case_eq (lt_dec(PDidx + 1) tableSize); intros.
    f_equal.
    apply proof_irrelevance.
    omega.
    unfold CIndex.
    case_eq(lt_dec (PDidx + 1) tableSize ); intros.

    assert(Hii : {| i := PDidx + 1; Hi := Pip_state.CIndex_obligation_1 (PDidx + 1) l0 |} = PRidx)

by trivial.
    contradict Hii.
    subst.
    unfold PDidx. unfold PRidx.
    unfold CIndex at 3.
    case_eq (lt_dec 0 tableSize); intros.
    unfold not; intros Hi.
    inversion Hi.
    assert(Hii : CIndex 2 + 1 = 0) by trivial.
    unfold CIndex in Hii.
    case_eq(lt_dec 0 tableSize); intros Hi1 Hi2;  rewrite Hi2 in *.
    inversion Hi.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    omega.
    omega.
    omega.
    omega.
    Qed.

        Lemma idxPRsucNotEqidxPD :
    PRidx + 1 < tableSize ->
    exists succidx1 : index, succIndexInternal PRidx = Some succidx1 /\ (succidx1 = PDidx -> False).
    Proof.
    unfold succIndexInternal.
    case_eq (lt_dec (PRidx + 1) tableSize); intros.
    eexists.
    split.
    instantiate (1:= CIndex (PRidx + 1)).
    f_equal.
    unfold CIndex .
    case_eq (lt_dec(PRidx + 1) tableSize); intros * Hc2.
    f_equal.
    apply proof_irrelevance.
    omega.
    unfold CIndex.
    case_eq(lt_dec (PRidx + 1) tableSize ); intros * Hc3 Hc4.
    contradict Hc4.
    subst.
    unfold PDidx. unfold PRidx.
    unfold CIndex at 3.
    case_eq (lt_dec 2 tableSize); intros * Hc5.
    unfold not; intros Hc6.
    inversion Hc6 as [Hc7].
    unfold CIndex in Hc7.
    case_eq(lt_dec 0 tableSize); intros * Hc8; rewrite Hc8 in *.
    inversion Hc6.
    simpl in *.
    omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    subst.
    omega.
    assert (tableSize > tableSizeLowerBound).
    apply tableSizeBigEnough.
    unfold tableSizeLowerBound in *.
    omega.
    omega.

    omega.
    Qed.

        Lemma idxPRidxPDNotEq : PRidx <> PDidx.
    Proof.
      unfold PDidx. unfold PRidx.
      apply indexEqFalse ;
      assert (tableSize > tableSizeLowerBound).
      apply tableSizeBigEnough.
      unfold tableSizeLowerBound in *.
      omega.  apply tableSizeBigEnough.
      unfold tableSizeLowerBound in *.
      omega. apply tableSizeBigEnough. omega.
      Qed.
*)

repo: dec


text:
From trillium.prelude Require Import classical.
From stdpp Require Import prelude.

Lemma make_proof_irrel (P : Prop) : ProofIrrel P.
Proof. intros ??; apply ProofIrrelevance. Qed.

Lemma make_decision P : Decision P.
Proof.
  assert (∃ x : Decision P, True) as Hdecex.
  { destruct (ExcludedMiddle P) as [HP|HnP].
    - exists (left HP); done.
    - exists (right HnP); done. }
  apply epsilon in Hdecex; done.
Qed.

author: logsem

repo: aneris

save_path: github-repos/coq/logsem-aneris


text:
From CTree Require Import
     CTree
     Eq
     Interp.Fold.

From RelationAlgebra Require Import
     monoid
     kat
     kat_tac
     prop
     rel
     srel
     comparisons
     rewriting
     normalisation.

From CTreeCCS Require Import
     Syntax
     Denotation
     Operational.

Import CCSNotations.
Import DenNotations.
Import OpNotations.
Open Scope ccs_scope.

Set Implicit Arguments.
Set Contextual Implicit.

Lemma SRep': forall P a P'
               (STEP : step a P P'),
    step a (!P) (P' ∥ !P).
Proof.
  intros * TR; apply SRep,SParL; auto.
Qed.

Lemma trans_nil_inv : forall l p, ~ trans l nil p.
Proof.
  intros * abs; eapply stuckS_is_stuck; apply abs.
Qed.

Definition ι : option action -> @label ccsE :=
  fun a => match a with
        | None => tau
        | Some a => comm a
        end.

Definition γ : @label ccsE -> option action :=
  fun l => match l with
        | val x => None
        | tau   => None
        | obs (Act a) _ => Some a
        end.

Lemma are_opposite_op : forall a, are_opposite a (op a).
Proof.
  unfold op, are_opposite.
  intros []; cbn; rewrite eqb_refl; auto.
Qed.

Lemma are_opposite_are_op : forall a b,
    are_opposite a b ->
    a = op b.
Proof.
  unfold are_opposite,op; intros [] []; cbn; intuition.
  all:destruct (c =? c0)%string eqn:EQ; try easy.
  all:apply eqb_eq in EQ; subst; auto.
Qed.

Lemma use_channel_can_comm : forall c a,
  use_channel c a = false <->
  can_comm c (ι a) = true.
Proof.
  unfold can_comm, use_channel.
  intros ? [[]|]; cbn; split; auto.
  all:match goal with |- context[if ?b then _ else _] => destruct b; easy end.
Qed.

Definition forward (R : term -> ccs -> Prop) : Prop :=
  forall P P' q a,
		R P q ->
		P ⊢ a →op P' ->
	  exists q', trans (ι a) q q' /\ R P' q'.

Definition backward (R : term -> ccs -> Prop) : Prop :=
  forall P q q' l,
		R P q ->
    trans l q q' ->
	  exists P', P ⊢ γ l →op P' /\ R P' q'.

Definition bisim R := forward R /\ backward R.
Definition bisimilar P q := exists R, bisim R /\ R P q.

Lemma bisimilar_bisim : bisim bisimilar.
Proof.
  split; red; intros * (R & BIS & HR) TR;
    pose proof BIS as [F B].
  - edestruct F as (? & ? & ?); eauto; eexists; split; eauto.
    exists R; split; auto.
  - edestruct B as (? & ? & ?); eauto; eexists; split; eauto.
    exists R; split; auto.
Qed.

Definition bisim_model := fun P (q: ccs) => ⟦P⟧ ~ q.

Lemma complete : forward bisim_model.
Proof.
  unfold bisim_model; red.
  intros * HR TR.
  revert q HR.
  induction TR; intros * HR; cbn in *.
  - step in HR. edestruct HR as [[? (? & TR & ? & ->)] [? ?]]; eauto.
    apply trans_prefix.
  - step in HR; edestruct HR as [[? (? & TR & ? & ->)] [? ?]]; eauto.
    apply trans_step.
  - edestruct IHTR as (q1 & TR1 & EQ1); eauto.
    step in HR; edestruct HR as [[? (? & ? & ? & ?)] [? (? & ? & ? & ?)]]; eauto.
    apply trans_plusL; apply TR1. (* Need to fix automation w.r.t. trans/transR *)
    cbn in *; subst.
    eexists; split; [apply H |].
    cbn; rewrite <- H0, <- EQ1; auto.
  - edestruct IHTR as (q2 & TR2 & EQ2); eauto.
    step in HR; edestruct HR as [[? (? & ? & ? & ->)] [? ?]].
    apply trans_plusR. apply TR2. (* Need to fix automation w.r.t. trans/transR *)
    eauto.
    eexists; split; [apply H |].
    cbn; rewrite <- H0, <- EQ2; auto.
  - edestruct IHTR as (q1 & TR1 & EQ1); eauto.
    step in HR; edestruct HR as [[? (? & ? & ? & ->)] [? ?]].
    pL; apply TR1. (* Need to fix automation w.r.t. trans/transR *)
    eauto.
    eexists; split; [apply H |].
    cbn; rewrite <- H0, <- EQ1; auto.
  - edestruct IHTR as (q2 & TR2 & EQ2); eauto.
    step in HR; edestruct HR as [[? (? & ? & ? & ->)] [? ?]].
    pR; apply TR2. (* Need to fix automation w.r.t. trans/transR *)
    eauto.
    eexists; split; [apply H |].
    cbn; rewrite <- H0, <- EQ2; auto.
  - edestruct IHTR1 as (q1 & TR1' & EQ1); eauto.
    edestruct IHTR2 as (q2 & TR2' & EQ2); eauto.
    step in HR; edestruct HR as [[? (? & ? & ? & ->)] [? ?]].
    pS; [apply TR1' | apply TR2' | apply are_opposite_op]. (* Need to fix automation w.r.t. trans/transR *)
    eauto.
    eexists; split; [apply H |].
    cbn; rewrite <- H0, <- EQ1, <- EQ2; auto.
  - edestruct IHTR as (q' & TR' & EQ'); eauto.
    eapply trans_new in TR' as (q'' & TR' & EQ''); [| apply use_channel_can_comm; eauto].
    step in HR;  edestruct HR as [[? (? & ? & ? & ->)] [? ?]].
    apply TR'.
    eauto.
    eexists; split.
    apply H.
    rewrite <- H0, EQ'', <- EQ'; auto.
  - rewrite unfold_bang', paraC in HR.
    exact (IHTR _ HR).
Qed.

Lemma correct : backward bisim_model.
Proof.
  unfold bisim_model; red.
  induction P; intros * HR TR; copy TR; step in HR; destruct HR as [_ B]; apply B in TR as [? (? & TR' & ? & ->)]; clear B; cbn in *.
  - exfalso; eapply trans_nil_inv,TR'.
  - apply trans_step_inv in TR' as [EQ ->].
    eexists; split; [constructor |].
    rewrite <- H, EQ; auto.
  - apply trans_prefix_inv in TR' as [EQ ->].
    eexists; split; [constructor |].
    rewrite <- H, EQ.
    auto.
  - trans_para_invT TR'.
    + edestruct IHP1 as (P' & STEP & EQ''); [reflexivity | apply TRp |].
      eexists; split.
      apply SParL; eauto.
      rewrite <- H,EQ,<-EQ''.
      auto.
    + edestruct IHP2 as (P' & STEP & EQ''); [reflexivity | apply TRq |].
      eexists; split.
      apply SParR; eauto.
      rewrite <- H,EQ,<-EQ''.
      auto.
    + edestruct IHP1 as (P' & STEP & EQ''); [reflexivity | apply TRp |].
      edestruct IHP2 as (P'' & STEP' & EQ'''); [reflexivity | apply TRq |].
      eexists; split.
      apply SPar with a.
      apply STEP.
      apply are_opposite_sym in Op.
      rewrite <- (are_opposite_are_op _ Op).
      apply STEP'.
      rewrite <- H,EQ,<-EQ'',<-EQ'''.
      auto.
  - apply trans_plus_inv in TR' as [(? & TRp & EQ) | (? & TRq & EQ)].
    + edestruct IHP1 as (P' & STEP & EQ''); [reflexivity | apply TRp |].
      eexists; split.
      apply SSumL; eauto.
      rewrite <- H,EQ,<-EQ''.
      auto.
    + edestruct IHP2 as (P' & STEP & EQ''); [reflexivity | apply TRq |].
      eexists; split.
      apply SSumR; eauto.
      rewrite <- H,EQ,<-EQ''.
      auto.
  - apply trans_new_inv in TR' as (p' & COM & TR & EQ).
    edestruct IHP as (P' & STEP & EQ''); [reflexivity | apply TR |].
    exists (P' ∖ c); split.
    apply SRes; auto.
    rewrite use_channel_can_comm.
    destruct l; auto; destruct e; auto.
    rewrite <- H,EQ,sb_guard, <-EQ''; auto.
  - trans_parabang_invT TR'.
    + edestruct IHP as (P' & STEP & EQ''); [reflexivity | apply TRp' |].
      exists (P' ∥ !P); split.
      apply SRep, SParL; auto.
      rewrite <- H,EQ,<-EQ''.
      rewrite parabang_eq.
      reflexivity.
    + edestruct IHP as (P' & STEP & EQ''); [reflexivity | apply TRq' |].
      rewrite EQ in H; clear x0 EQ.
      exists (P' ∥ !P); split.
      apply SRep, SParL; auto.
      rewrite <- H, <-EQ''.
      cbn.
      rewrite (paraC ⟦P⟧), parabang_aux, parabang_eq.
      auto.
    + edestruct IHP as (P' & STEP & EQ''); [reflexivity | apply TRp' |].
      edestruct IHP as (P'' & STEP' & EQ'''); [reflexivity | apply TRq' |].
      exists (P' ∥ (P'' ∥ !P)).
      split.
      apply SRep.
      apply SPar with a.
      apply STEP.
      apply are_opposite_sym in Op.
      rewrite <- (are_opposite_are_op _ Op).
      apply SRep', STEP'.
      rewrite <- H,EQ,<-EQ'',<-EQ'''.
      rewrite parabang_eq.
      cbn.
      rewrite paraA; auto.
    + edestruct IHP as (P' & STEP & EQ''); [reflexivity | apply TRq' |].
      edestruct IHP as (P'' & STEP' & EQ'''); [reflexivity | apply TRq'' |].
      rewrite EQ in H; clear x0 EQ.
      rewrite <- EQ'', <- EQ''' in H.
      rewrite paraC, parabang_aux, parabang_eq in H.
      exists (P' ∥ (P'' ∥ !P)).
      split.
      apply SRep.
      apply SPar with a.
      apply STEP.
      apply are_opposite_sym in Op.
      rewrite <- (are_opposite_are_op _ Op).
      apply SRep', STEP'.
      rewrite <- H; cbn; rewrite paraA; auto.
Qed.

Theorem term_model_bisimilar : forall P, bisimilar P ⟦P⟧.
Proof.
  exists bisim_model; split; red; auto using correct,complete.
Qed.

(* We depend currently on
   - [Eqdep.Eq_rect_eq.eq_rect_eq]
 *)
Print Assumptions term_model_bisimilar.

Definition forward_inv (R : ccs -> term -> Prop) : Prop :=
  forall p p' Q l,
    R p Q ->
    trans l p p' ->
    exists Q', Q ⊢ γ l →op Q' /\ R p' Q'.

Definition backward_inv (R : ccs -> term -> Prop) : Prop :=
  forall p Q Q' a,
    R p Q ->
    Q ⊢ a →op Q' ->
    exists p', trans (ι a) p p' /\ R p' Q'.

Definition bisim_inv R := forward_inv R /\ backward_inv R.
Definition bisimilar_inv t u := exists R, bisim_inv R /\ R t u.

Lemma bisimilar_inv_bisim_inv : bisim_inv bisimilar_inv.
Proof.
 split; red; intros * (R & BIS & HR) TR;
    pose proof BIS as [F B].
  - edestruct F as (? & ? & ?); eauto; eexists; split; eauto.
    exists R; split; auto.
  - edestruct B as (? & ? & ?); eauto; eexists; split; eauto.
    exists R; split; auto.
Qed.

Definition rev {A B} (R : A -> B -> Prop) : B -> A -> Prop := fun b a => R a b.

Lemma bisim_bisim_inv : forall R, bisim R -> bisim_inv (rev R).
Proof.
  intros ? [F B]; split; red; unfold rev; cbn; intros * HR TR.
  edestruct B; eauto.
  edestruct F; eauto.
Qed.

Lemma term_model_bisimilar_inv : forall P, bisimilar_inv ⟦P⟧ P.
Proof.
  intros P; edestruct (@term_model_bisimilar P) as (R & BIS & HR); eauto.
  eexists; split.
  apply bisim_bisim_inv; eauto.
  auto.
Qed.

Lemma ιγ : forall l (t u : ccs),
    trans l t u ->
    ι (γ l) = l.
Proof.
  intros [] ? ? TR; cbn; auto.
  destruct e,v; auto.
  eapply trans_val_invT in TR; subst; destruct v.
Qed.

Lemma γι : forall l,
    γ (ι l) = l.
Proof.
  intros []; auto.
Qed.

(* Naming *)
Lemma cross_model_compose : forall T t u U,
    bisimilar t T ->
    Operational.bisim t u ->
    bisimilar u U ->
    T ~ U.
Proof.
  coinduction ? ?.
  intros * EQtT EQtu EQuU.
  pose proof bisimilar_bisim as [F B].
  step in EQtu; destruct EQtu as [F' B'].
  split; intros ? ? TRTt.
  - edestruct B as (T' & TRT' & ?); [apply EQtT | |]; eauto.
    edestruct F' as [U' TRU' ?]; eauto.
    edestruct F as (u' & TRu' & ?); [apply EQuU | |]; eauto.
    erewrite ιγ in TRu'.
    do 2 eexists; split; eauto.
    eapply TRTt.
  - edestruct B as (T' & TRT' & ?); [apply EQuU | |]; eauto.
    edestruct B' as [U' TRU' ?]; eauto.
    edestruct F as (u' & TRu' & ?); [apply EQtT | |]; eauto.
    erewrite ιγ in TRu'; eauto.
    do 2 eexists; split; [|split]; cbn in *; eauto.
Qed.

Lemma cross_model_compose' : forall T t u U,
    bisimilar t T ->
    T ~ U ->
    bisimilar u U ->
    Operational.bisim t u.
Proof.
  coinduction ? ?.
  intros * EQtT EQtu EQuU.
  pose proof bisimilar_bisim as [F B].
  step in EQtu; destruct EQtu as [F' B'].
  split; intros ? ? TRTt.
  - edestruct F as (T' & TRT' & ?); [apply EQtT | |]; eauto.
    edestruct F' as [U' (? & TRU' & ? & <-)]; eauto.
    edestruct B as (u' & TRu' & ?); [apply EQuU | |]; eauto.
    erewrite γι in TRu'; eauto.
  - edestruct F as (T' & TRT' & ?); [apply EQuU | |]; eauto.
    edestruct B' as [U' (? & TRU' & ? & ?)]; cbn in *; subst; eauto.
    edestruct B as (u' & TRu' & ?); [apply EQtT | |]; eauto.
    erewrite γι in TRu'; eauto.
Qed.

Lemma bisimilar_bisimilar_inv : forall t T,
    bisimilar_inv t T -> bisimilar T t.
Proof.
  intros * (R & [F B] & HR).
  exists (rev R); split; [| apply HR].
  split.
  red; intros; edestruct B; eauto.
  red; intros; edestruct F; eauto.
Qed.

Lemma embed_sound : forall t u, Operational.bisim t u -> ⟦t⟧ ~ ⟦u⟧.
Proof.
  intros * BIS.
  apply (gfp_fp b t u) in BIS; destruct BIS as [F B]; cbn in *.
  step; split.
  - intros ? T' TR.
    pose proof (@term_model_bisimilar t) as BISt.
    pose proof (@term_model_bisimilar u) as BISu.
    pose proof bisimilar_bisim as [F' B'].
    edestruct B' as (t' & TRt & EQTt); [apply BISt | ..]; eauto.
    edestruct F as [u' TR'' EQtu]; eauto.
    edestruct F' as (U' & TRu & EQuU); [apply BISu |..]; eauto.
    erewrite ιγ in TRu; eauto.
    do 2 eexists; split; [|split]; eauto.
    eapply cross_model_compose; eauto.
  - intros ? U' TR.
    pose proof (@term_model_bisimilar_inv u) as BISu.
    pose proof (@term_model_bisimilar_inv t) as BISt.
    pose proof bisimilar_inv_bisim_inv as [F' B'].
    cbn.
    edestruct F' as (u' & TRu & EQuU); [apply BISu |..]; eauto.
    edestruct B as [t' TR'' EQtu]; eauto.
    edestruct B' as (T' & TRT & EQuT); [apply BISt |..]; eauto.
    erewrite ιγ in TRT; eauto.
    do 2 eexists; split; [|split]; eauto.
    apply bisimilar_bisimilar_inv in EQuU, EQuT.
    eapply cross_model_compose; eauto.
Qed.

Lemma embed_complete : forall t u, ⟦t⟧ ~ ⟦u⟧ -> Operational.bisim t u.
Proof.
  intros * BIS.
  step in BIS; destruct BIS as [F B]; cbn in *.
  step; split.
  - intros ? T' TR.
    pose proof (@term_model_bisimilar t) as BISt.
    pose proof (@term_model_bisimilar u) as BISu.
    pose proof bisimilar_bisim as [F' B'].
    edestruct F' as (t' & TRt & EQTt); [apply BISt | ..]; eauto.
    edestruct F as [u' (? & TR'' & ? & <-)]; eauto.
    edestruct B' as (U' & TRu & EQuU); [apply BISu |..]; eauto.
    erewrite γι in TRu; eauto.
    eexists. apply TRu.
    eapply cross_model_compose'; eauto.
  - intros ? U' TR.
    pose proof (@term_model_bisimilar_inv u) as BISu.
    pose proof (@term_model_bisimilar_inv t) as BISt.
    pose proof bisimilar_inv_bisim_inv as [F' B'].
    cbn.
    edestruct B' as (u' & TRu & EQuU); [apply BISu |..]; eauto.
    edestruct B as [t' (? & TR'' & ? & ->)]; eauto.
    edestruct F' as (T' & TRT & EQuT); [apply BISt |..]; eauto.
    erewrite γι in TRT; eauto.
    eexists. apply TRT.
    apply bisimilar_bisimilar_inv in EQuU, EQuT.
    eapply cross_model_compose'; eauto.
Qed.

Theorem equiv_bisims : forall t u, ⟦t⟧ ~ ⟦u⟧ <-> Operational.bisim t u.
Proof.
  intros; split; eauto using embed_complete, embed_sound.
Qed.

author: vellvm

repo: ctrees

save_path: github-repos/coq/vellvm-ctrees