text:
Require Import Ensembles.
Require Import Coq.Lists.List.
Require Import primRec.
Require Import cPair.
Require Import Arith.
Require Import folProp.
Require Import code.
Require Import codeList.
Require Import codeFreeVar.
Require Import extEqualNat.
Require Vector.
Require Import prLogic.

Section close.

Variable L : Language.
Variable codeF : Functions L -> nat.
Variable codeR : Relations L -> nat.

Let Formula := Formula L.
Let codeFormula := codeFormula L codeF codeR.

Definition codeCloseList : nat -> nat -> nat :=
  evalStrongRec 1
    (fun l recs f : nat =>
     switchPR l
       (cPair 3
          (cPair (cPairPi1 (pred l))
             (codeNth (l - S (cPairPi2 (pred l))) recs))) f).

Lemma codeCloseListCorrect :
 forall (l : list nat) (f : Formula),
 codeCloseList (codeList l) (codeFormula f) = codeFormula (closeList L l f).
Proof.
intros.
set
 (g :=
  fun l recs f : nat =>
  switchPR l
    (cPair 3
       (cPair (cPairPi1 (pred l)) (codeNth (l - S (cPairPi2 (pred l))) recs)))
    f) in *.
induction l as [| a l Hrecl].
simpl in |- *.
unfold codeCloseList in |- *.
unfold evalStrongRec in |- *.
simpl in |- *.
rewrite cPairProjections1.
reflexivity.
simpl in |- *.
unfold codeCloseList in |- *.
fold g in |- *.
assert
 (forall n m : nat,
  m < n ->
  extEqual 1
    (evalComposeFunc 1 1 (Vector.cons _ (evalStrongRecHelp 1 g n) 0 (Vector.nil _))
       (fun b : nat => codeNth (n - S m) b)) (evalStrongRec 1 g m)).
intros.
apply (evalStrongRecHelp2 1).
assumption.
simpl in H.
unfold evalStrongRec in |- *.
unfold evalComposeFunc, evalOneParamList, evalList in |- *.
rewrite computeEvalStrongRecHelp.
unfold compose2 in |- *.
unfold evalComposeFunc, evalOneParamList, evalList in |- *.
unfold g at 1 in |- *.
rewrite H.
simpl in |- *.
repeat rewrite cPairProjections1 || rewrite cPairProjections2.
rewrite <- Hrecl.
reflexivity.
simpl in |- *.
apply le_lt_n_Sm.
apply cPairLe2A.
Qed.

Lemma codeCloseListIsPR : isPR 2 codeCloseList.
Proof.
intros.
unfold codeCloseList in |- *.
apply evalStrongRecIsPR.
apply
 compose3_3IsPR
  with
    (f1 := fun l recs f : nat => l)
    (f2 := fun l recs f : nat =>
           cPair 3
             (cPair (cPairPi1 (pred l))
                (codeNth (l - S (cPairPi2 (pred l))) recs)))
    (f3 := fun l recs f : nat => f).
apply pi1_3IsPR.
apply
 filter110IsPR
  with
    (g := fun l recs : nat =>
          cPair 3
            (cPair (cPairPi1 (pred l))
               (codeNth (l - S (cPairPi2 (pred l))) recs))).
apply
 compose2_2IsPR
  with
    (f := fun l recs : nat => 3)
    (g := fun l recs : nat =>
          cPair (cPairPi1 (pred l))
            (codeNth (l - S (cPairPi2 (pred l))) recs)).
apply filter10IsPR with (g := fun _ : nat => 3).
apply const1_NIsPR.
apply
 compose2_2IsPR
  with
    (f := fun l recs : nat => cPairPi1 (pred l))
    (g := fun l recs : nat => codeNth (l - S (cPairPi2 (pred l))) recs).
apply filter10IsPR with (g := fun l : nat => cPairPi1 (pred l)).
apply compose1_1IsPR.
apply predIsPR.
apply cPairPi1IsPR.
apply callIsPR with (g := fun l : nat => cPairPi2 (pred l)).
apply compose1_1IsPR.
apply predIsPR.
apply cPairPi2IsPR.
apply cPairIsPR.
apply cPairIsPR.
apply pi3_3IsPR.
apply switchIsPR.
Qed.

Definition codeClose (f : nat) : nat :=
  codeCloseList (codeNoDup (codeFreeVarFormula f)) f.

Lemma codeCloseCorrect :
 forall f : Formula, codeClose (codeFormula f) = codeFormula (close L f).
Proof.
intros.
unfold close in |- *.
unfold codeClose in |- *.
unfold codeFormula in |- *.
rewrite codeFreeVarFormulaCorrect.
rewrite codeNoDupCorrect.
apply codeCloseListCorrect.
Qed.

Lemma codeCloseIsPR : isPR 1 codeClose.
Proof.
unfold codeClose in |- *.
apply
 compose1_2IsPR
  with
    (f := fun f : nat => codeNoDup (codeFreeVarFormula f))
    (f' := fun f : nat => f).
apply compose1_1IsPR.
apply codeFreeVarFormulaIsPR.
apply codeNoDupIsPR.
apply idIsPR.
apply codeCloseListIsPR.
Qed.

End close.

Require Import PA.
Require Import codeSubFormula.

Section Code_PA.

Let codeTerm := codeTerm LNT codeLNTFunction.
Let codeFormula := codeFormula LNT codeLNTFunction codeLNTRelation.
Let codeFormulaInj :=
  codeFormulaInj LNT codeLNTFunction codeLNTRelation codeLNTFunctionInj
    codeLNTRelationInj.

Definition codeOpen : nat -> nat :=
  evalStrongRec 0
    (fun f recs : nat =>
     switchPR (cPairPi1 f)
       (switchPR (pred (cPairPi1 f))
          (switchPR (pred (pred (cPairPi1 f)))
             (switchPR (pred (pred (pred (cPairPi1 f)))) f
                (codeNth (f - S (cPairPi2 (cPairPi2 f))) recs)) f) f) f).

Lemma codeOpenCorrect :
 forall f : Formula, codeOpen (codeFormula f) = codeFormula (open f).
Proof.
intros.
unfold codeOpen, open in |- *.
set
 (g :=
  fun f recs : nat =>
  switchPR (cPairPi1 f)
    (switchPR (pred (cPairPi1 f))
       (switchPR (pred (pred (cPairPi1 f)))
          (switchPR (pred (pred (pred (cPairPi1 f)))) f
             (codeNth (f - S (cPairPi2 (cPairPi2 f))) recs)) f) f) f)
 in *.
induction f as [t t0| r t| f1 Hrecf1 f0 Hrecf0| f Hrecf| n f Hrecf];
 simpl in |- *; unfold evalStrongRec in |- *.
simpl in |- *; unfold g at 1 in |- *;
 repeat rewrite cPairProjections1 || rewrite cPairProjections2;
 reflexivity.
simpl in |- *; unfold g at 1 in |- *;
 repeat rewrite cPairProjections1 || rewrite cPairProjections2;
 reflexivity.
simpl in |- *; unfold g at 1 in |- *;
 repeat rewrite cPairProjections1 || rewrite cPairProjections2;
 reflexivity.
simpl in |- *; unfold g at 1 in |- *;
 repeat rewrite cPairProjections1 || rewrite cPairProjections2;
 reflexivity.
unfold evalComposeFunc, evalOneParamList, evalList in |- *.
rewrite computeEvalStrongRecHelp.
unfold compose2 in |- *.
unfold evalComposeFunc, evalOneParamList, evalList in |- *.
unfold g at 1 in |- *.
repeat rewrite evalStrongRecHelp1.
unfold pred in |- *.
repeat rewrite cPairProjections1 || rewrite cPairProjections2.
simpl in |- *.
apply Hrecf.
eapply le_lt_trans.
apply cPairLe2A.
rewrite cPairProjections2.
apply cPairLt2.
Qed.

Lemma codeOpenIsPR : isPR 1 codeOpen.
Proof.
unfold codeOpen in |- *.
apply evalStrongRecIsPR.
apply
 compose2_3IsPR
  with
    (f1 := fun f recs : nat => cPairPi1 f)
    (f2 := fun f recs : nat =>
           switchPR (pred (cPairPi1 f))
             (switchPR (pred (pred (cPairPi1 f)))
                (switchPR (pred (pred (pred (cPairPi1 f)))) f
                   (codeNth (f - S (cPairPi2 (cPairPi2 f))) recs)) f) f)
    (f3 := fun f recs : nat => f).
apply filter10IsPR.
apply cPairPi1IsPR.
apply
 compose2_3IsPR
  with
    (f1 := fun f recs : nat => pred (cPairPi1 f))
    (f2 := fun f recs : nat =>
           switchPR (pred (pred (cPairPi1 f)))
             (switchPR (pred (pred (pred (cPairPi1 f)))) f
                (codeNth (f - S (cPairPi2 (cPairPi2 f))) recs)) f)
    (f3 := fun f recs : nat => f).
apply filter10IsPR with (g := fun f : nat => pred (cPairPi1 f)).
apply compose1_1IsPR.
apply cPairPi1IsPR.
apply predIsPR.
apply
 compose2_3IsPR
  with
    (f1 := fun f recs : nat => pred (pred (cPairPi1 f)))
    (f2 := fun f recs : nat =>
           switchPR (pred (pred (pred (cPairPi1 f)))) f
             (codeNth (f - S (cPairPi2 (cPairPi2 f))) recs))
    (f3 := fun f recs : nat => f).
apply filter10IsPR with (g := fun f : nat => pred (pred (cPairPi1 f))).
apply compose1_1IsPR with (f := fun f : nat => pred (cPairPi1 f)).
apply compose1_1IsPR.
apply cPairPi1IsPR.
apply predIsPR.
apply predIsPR.
apply
 compose2_3IsPR
  with
    (f1 := fun f recs : nat => pred (pred (pred (cPairPi1 f))))
    (f2 := fun f recs : nat => f)
    (f3 := fun f recs : nat => codeNth (f - S (cPairPi2 (cPairPi2 f))) recs).
apply filter10IsPR with (g := fun f : nat => pred (pred (pred (cPairPi1 f)))).
apply compose1_1IsPR with (f := fun f : nat => pred (pred (cPairPi1 f))).
apply compose1_1IsPR with (f := fun f : nat => pred (cPairPi1 f)).
apply compose1_1IsPR.
apply cPairPi1IsPR.
apply predIsPR.
apply predIsPR.
apply predIsPR.
apply pi1_2IsPR.
apply callIsPR with (g := fun f : nat => cPairPi2 (cPairPi2 f)).
apply compose1_1IsPR; apply cPairPi2IsPR.
apply switchIsPR.
apply pi1_2IsPR.
apply switchIsPR.
apply pi1_2IsPR.
apply switchIsPR.
apply pi1_2IsPR.
apply switchIsPR.
Qed.

Definition codeInductionSchema (f : nat) : bool :=
  let n :=
    cPairPi1
      (cPairPi2 (cPairPi2 (cPairPi2 (cPairPi2 (cPairPi2 (codeOpen f)))))) in
  let g :=
    cPairPi2
      (cPairPi2 (cPairPi2 (cPairPi2 (cPairPi2 (cPairPi2 (codeOpen f)))))) in
  beq_nat
    (codeClose
       (codeImp (codeSubFormula g n (codeTerm Zero))
          (codeImp
             (codeForall n
                (codeImp g (codeSubFormula g n (codeTerm (Succ (var n))))))
             (codeForall n g)))) f.

Lemma codeInductionSchemaCorrect1 :
 forall f : Formula,
 InductionSchema f -> codeInductionSchema (codeFormula f) = true.
Proof.
intros.
induction H as (x, H).
induction H as (x0, H).
unfold PA7 in H.
rewrite H.
clear H f.
lazy beta delta [codeInductionSchema] in |- *.
rewrite codeOpenCorrect.
replace
 (open
    (close LNT
       (impH (substituteFormula LNT x x0 Zero)
          (impH
             (forallH x0
                (impH x (substituteFormula LNT x x0 (Succ (var x0)))))
             (forallH x0 x))))) with
 (impH (substituteFormula LNT x x0 Zero)
    (impH (forallH x0 (impH x (substituteFormula LNT x x0 (Succ (var x0)))))
       (forallH x0 x))).
replace
 (cPairPi1
    (cPairPi2
       (cPairPi2
          (cPairPi2
             (cPairPi2
                (cPairPi2
                   (codeFormula
                      (impH (substituteFormula LNT x x0 Zero)
                         (impH
                            (forallH x0
                               (impH x
                                  (substituteFormula LNT x x0 (Succ (var x0)))))
                            (forallH x0 x)))))))))) with x0.
replace
 (cPairPi2
    (cPairPi2
       (cPairPi2
          (cPairPi2
             (cPairPi2
                (cPairPi2
                   (codeFormula
                      (impH (substituteFormula LNT x x0 Zero)
                         (impH
                            (forallH x0
                               (impH x
                                  (substituteFormula LNT x x0 (Succ (var x0)))))
                            (forallH x0 x)))))))))) with
 (codeFormula x).
cbv zeta in |- *.
unfold codeFormula in |- *.
rewrite <- codeCloseCorrect.
replace
 (codeClose
    (codeImp
       (codeSubFormula
          (code.codeFormula LNT codeLNTFunction codeLNTRelation x) x0
          (codeTerm Zero))
       (codeImp
          (codeForall x0
             (codeImp
                (code.codeFormula LNT codeLNTFunction codeLNTRelation x)
                (codeSubFormula
                   (code.codeFormula LNT codeLNTFunction codeLNTRelation x)
                   x0 (codeTerm (Succ (var x0))))))
          (codeForall x0
             (code.codeFormula LNT codeLNTFunction codeLNTRelation x)))))
 with
 (codeClose
    (code.codeFormula LNT codeLNTFunction codeLNTRelation
       (impH (substituteFormula LNT x x0 Zero)
          (impH
             (forallH x0
                (impH x (substituteFormula LNT x x0 (Succ (var x0)))))
             (forallH x0 x))))).
rewrite <- beq_nat_refl.
reflexivity.
simpl in |- *.
unfold codeTerm in |- *.
repeat rewrite codeSubFormulaCorrect.
reflexivity.
simpl in |- *.
repeat rewrite cPairProjections1 || rewrite cPairProjections2.
reflexivity.
simpl in |- *.
repeat rewrite cPairProjections1 || rewrite cPairProjections2.
reflexivity.
unfold close in |- *.
induction
 (ListExt.no_dup nat eq_nat_dec
    (freeVarFormula LNT
       (impH (substituteFormula LNT x x0 Zero)
          (impH
             (forallH x0
                (impH x (substituteFormula LNT x x0 (Succ (var x0)))))
             (forallH x0 x))))).
reflexivity.
simpl in |- *.
assumption.
Qed.

Lemma codeInductionSchemaCorrect2 :
 forall f : Formula,
 codeInductionSchema (codeFormula f) = true -> InductionSchema f.
Proof.
intros.
lazy beta delta [codeInductionSchema] in H.
rewrite codeOpenCorrect in H.
set
 (n :=
  cPairPi1
    (cPairPi2
       (cPairPi2 (cPairPi2 (cPairPi2 (cPairPi2 (codeFormula (open f))))))))
 in *.
set
 (g :=
  cPairPi2
    (cPairPi2
       (cPairPi2 (cPairPi2 (cPairPi2 (cPairPi2 (codeFormula (open f))))))))
 in *.
cbv zeta in H.
induction
 (eq_nat_dec
    (codeImp (codeSubFormula g n (codeTerm Zero))
       (codeImp
          (codeForall n
             (codeImp g (codeSubFormula g n (codeTerm (Succ (var n))))))
          (codeForall n g))) (codeFormula (open f))).
rewrite a in H.
unfold codeFormula in H.
rewrite codeCloseCorrect in H.
fold codeFormula in H.
induction (formula_dec LNT LNT_dec (close LNT (open f)) f).
unfold codeImp at 1 in a.
destruct (open f) as [t t0| r t| f0 f1| f0| n0 f0]; simpl in a;
 try
  match goal with
  | h:(cPair ?X1 ?X2 = cPair ?X3 ?X4) |- _ =>
      elimtype False; cut (X1 = X3);
       [ discriminate | eapply cPairInj1; apply h ]
  end.
assert (codeSubFormula g n (codeTerm Zero) = codeFormula f0).
eapply cPairInj1.
eapply cPairInj2.
apply a.
assert
 (codeImp
    (codeForall n (codeImp g (codeSubFormula g n (codeTerm (Succ (var n))))))
    (codeForall n g) = codeFormula f1).
eapply cPairInj2.
eapply cPairInj2.
apply a.
clear a.
Opaque cPairPi1.
Opaque cPairPi2.
unfold codeImp at 1 in H1.
destruct f1 as [t t0| r t| f1 f2| f1| n0 f1]; simpl in H1;
 try
  match goal with
  | h:(cPair ?X1 ?X2 = cPair ?X3 ?X4) |- _ =>
      elimtype False; cut (X1 = X3);
       [ discriminate | eapply cPairInj1; apply h ]
  end.
assert
 (codeForall n (codeImp g (codeSubFormula g n (codeTerm (Succ (var n))))) =
  codeFormula f1).
eapply cPairInj1.
eapply cPairInj2.
apply H1.
assert (codeForall n g = codeFormula f2).
eapply cPairInj2.
eapply cPairInj2.
apply H1.
clear H1.
unfold codeForall at 1 in H3.
destruct f2 as [t t0| r t| f2 f3| f2| n0 f2]; simpl in H3;
 try
  match goal with
  | h:(cPair ?X1 ?X2 = cPair ?X3 ?X4) |- _ =>
      elimtype False; cut (X1 = X3);
       [ discriminate | eapply cPairInj1; apply h ]
  end.
simpl in (value of n).
simpl in (value of g).
unfold InductionSchema in |- *.
exists f2.
exists n0.
unfold PA7 in |- *.
replace (substituteFormula LNT f2 n0 Zero) with f0.
replace (forallH n0 (impH f2 (substituteFormula LNT f2 n0 (Succ (var n0)))))
 with f1.
symmetry  in |- *.
apply a0.
apply codeFormulaInj.
simpl in |- *.
rewrite <- codeSubFormulaCorrect.
symmetry  in |- *.
unfold n, g in H2.
repeat rewrite cPairProjections1 in H2 || rewrite cPairProjections2 in H2.
apply H2.
apply codeFormulaInj.
rewrite <- codeSubFormulaCorrect.
symmetry  in |- *.
unfold n, g in H0.
repeat rewrite cPairProjections1 in H0 || rewrite cPairProjections2 in H0.
apply H0.
rewrite beq_nat_not_refl in H.
discriminate H.
unfold not in |- *; intros; apply b.
apply codeFormulaInj.
apply H0.
rewrite beq_nat_not_refl in H.
discriminate H.
unfold not in |- *; intros; apply b.
rewrite <- codeOpenCorrect.
rewrite <- H0.
unfold codeImp in |- *.
generalize
 (cPair (codeSubFormula g n (codeTerm Zero))
    (cPair 1
       (cPair
          (codeForall n
             (cPair 1
                (cPair g (codeSubFormula g n (codeTerm (Succ (var n)))))))
          (codeForall n g)))).
intros.
unfold codeClose in |- *.
assert
 (forall m : nat,
  m <= codeNoDup (codeFreeVarFormula (cPair 1 n0)) ->
  cPair 1 n0 = codeOpen (codeCloseList m (cPair 1 n0))).
induction (codeNoDup (codeFreeVarFormula (cPair 1 n0))).
intros.
rewrite <- (le_n_O_eq _ H1).
unfold codeCloseList in |- *.
unfold evalStrongRec in |- *.
unfold evalComposeFunc, evalOneParamList, evalList in |- *.
simpl in |- *.
rewrite cPairProjections1.
unfold codeOpen in |- *.
unfold evalStrongRec in |- *.
unfold evalComposeFunc, evalOneParamList, evalList in |- *.
rewrite computeEvalStrongRecHelp.
unfold compose2 in |- *.
unfold evalComposeFunc, evalOneParamList, evalList in |- *.
repeat rewrite cPairProjections1.
simpl in |- *.
repeat rewrite cPairProjections1.
reflexivity.
intros.
induction (le_lt_or_eq _ _ H1).
apply IHn1.
apply lt_n_Sm_le.
assumption.
rewrite H2.
unfold codeCloseList in |- *.
set
 (g0 :=
  fun l recs f0 : nat =>
  switchPR l
    (cPair 3
       (cPair (cPairPi1 (pred l)) (codeNth (l - S (cPairPi2 (pred l))) recs)))
    f0) in *.
unfold evalStrongRec in |- *.
unfold evalComposeFunc, evalOneParamList, evalList in |- *.
rewrite computeEvalStrongRecHelp.
unfold compose2 in |- *.
unfold evalComposeFunc, evalOneParamList, evalList in |- *.
assert
 (forall n m : nat,
  m < n ->
  extEqual 1
    (evalComposeFunc 1 1 (Vector.cons _ (evalStrongRecHelp 1 g0 n) 0 (Vector.nil _))
       (fun b : nat => codeNth (n - S m) b)) (evalStrongRec 1 g0 m)).
intros.
apply (evalStrongRecHelp2 1).
assumption.
simpl in H3.
unfold g0 at 1 in |- *.
rewrite H3.
simpl in |- *.
repeat rewrite cPairProjections1.
unfold codeCloseList in IHn1.
move g0 after IHn1; fold g0 in IHn1.
set (A := evalStrongRec 1 g0 (cPairPi2 n1) (cPair 1 n0)) in *.
unfold codeOpen in |- *.
set
 (g1 :=
  fun f0 recs : nat =>
  switchPR (cPairPi1 f0)
    (switchPR (pred (cPairPi1 f0))
       (switchPR (pred (pred (cPairPi1 f0)))
          (switchPR (pred (pred (pred (cPairPi1 f0)))) f0
             (codeNth (f0 - S (cPairPi2 (cPairPi2 f0))) recs)) f0) f0) f0)
 in *.
unfold evalStrongRec in |- *.
unfold evalComposeFunc, evalOneParamList, evalList in |- *.
rewrite computeEvalStrongRecHelp.
unfold compose2 in |- *.
unfold evalComposeFunc, evalOneParamList, evalList in |- *.
unfold g1 at 1 in |- *.
unfold pred at 1 in |- *.
repeat rewrite cPairProjections1.
repeat rewrite evalStrongRecHelp1.
simpl in |- *.
repeat rewrite cPairProjections2.
unfold A in |- *.
unfold codeOpen in IHn1.
move g1 after IHn1; fold g1 in IHn1.
apply IHn1.
apply cPairLe2A.
repeat rewrite cPairProjections2.
eapply le_lt_trans; [ idtac | apply cPairLt2 ].
apply cPairLe2.
simpl in |- *.
apply le_lt_n_Sm.
apply cPairLe2A.
apply H1.
apply le_n.
Qed.

Lemma codeInductionSchemaCorrect3 :
 forall f : Formula,
 ~ InductionSchema f -> codeInductionSchema (codeFormula f) = false.
Proof.
intros.
assert (forall x : bool, x = true \/ x = false).
intros.
induction x; auto.
induction (H0 (codeInductionSchema (codeFormula f))).
elim H.
apply codeInductionSchemaCorrect2.
assumption.
assumption.
Qed.

Lemma codeInductionSchemaIsPR : isPRrel 1 codeInductionSchema.
Proof.
lazy beta delta [codeInductionSchema] in |- *.
set
 (A :=
  fun f : nat =>
  cPairPi2 (cPairPi2 (cPairPi2 (cPairPi2 (cPairPi2 (codeOpen f))))))
 in *.
assert (isPR 1 A).
unfold A in |- *.
apply compose1_1IsPR with (g := iterate cPairPi2 5) (f := codeOpen).
apply codeOpenIsPR.
apply iterateIsPR.
apply cPairPi2IsPR.
assert
 (isPRrel 1
    (fun f : nat =>
     let n := cPairPi1 (A f) in
     let g := cPairPi2 (A f) in
     beq_nat
       (codeClose
          (codeImp (codeSubFormula g n (codeTerm Zero))
             (codeImp
                (codeForall n
                   (codeImp g (codeSubFormula g n (codeTerm (Succ (var n))))))
                (codeForall n g)))) f)).
unfold isPRrel in |- *.
apply
 compose1_2IsPR
  with
    (g := charFunction 2 beq_nat)
    (f' := fun f : nat => f)
    (f := fun f : nat =>
          codeClose
            (codeImp
               (codeSubFormula (cPairPi2 (A f)) (cPairPi1 (A f))
                  (codeTerm Zero))
               (codeImp
                  (codeForall (cPairPi1 (A f))
                     (codeImp (cPairPi2 (A f))
                        (codeSubFormula (cPairPi2 (A f))
                           (cPairPi1 (A f))
                           (codeTerm (Succ (var (cPairPi1 (A f))))))))
                  (codeForall (cPairPi1 (A f)) (cPairPi2 (A f)))))).
apply
 compose1_1IsPR
  with
    (f := fun f : nat =>
          codeImp
            (codeSubFormula (cPairPi2 (A f)) (cPairPi1 (A f)) (codeTerm Zero))
            (codeImp
               (codeForall (cPairPi1 (A f))
                  (codeImp (cPairPi2 (A f))
                     (codeSubFormula (cPairPi2 (A f))
                        (cPairPi1 (A f))
                        (codeTerm (Succ (var (cPairPi1 (A f))))))))
               (codeForall (cPairPi1 (A f)) (cPairPi2 (A f))))).
apply
 compose1_2IsPR
  with
    (f := fun f : nat =>
          codeSubFormula (cPairPi2 (A f)) (cPairPi1 (A f)) (codeTerm Zero))
    (f' := fun f : nat =>
           codeImp
             (codeForall (cPairPi1 (A f))
                (codeImp (cPairPi2 (A f))
                   (codeSubFormula (cPairPi2 (A f))
                      (cPairPi1 (A f))
                      (codeTerm (Succ (var (cPairPi1 (A f))))))))
             (codeForall (cPairPi1 (A f)) (cPairPi2 (A f)))).
apply
 compose1_3IsPR
  with
    (f1 := fun f : nat => cPairPi2 (A f))
    (f2 := fun f : nat => cPairPi1 (A f))
    (f3 := fun f : nat => codeTerm Zero).
apply compose1_1IsPR.
assumption.
apply cPairPi2IsPR.
apply compose1_1IsPR.
assumption.
apply cPairPi1IsPR.
apply const1_NIsPR.
apply codeSubFormulaIsPR.
apply
 compose1_2IsPR
  with
    (f := fun f : nat =>
          codeForall (cPairPi1 (A f))
            (codeImp (cPairPi2 (A f))
               (codeSubFormula (cPairPi2 (A f)) (cPairPi1 (A f))
                  (codeTerm (Succ (var (cPairPi1 (A f))))))))
    (f' := fun f : nat => codeForall (cPairPi1 (A f)) (cPairPi2 (A f))).
apply
 compose1_2IsPR
  with
    (f := fun f : nat => cPairPi1 (A f))
    (f' := fun f : nat =>
           codeImp (cPairPi2 (A f))
             (codeSubFormula (cPairPi2 (A f)) (cPairPi1 (A f))
                (codeTerm (Succ (var (cPairPi1 (A f))))))).
apply compose1_1IsPR.
assumption.
apply cPairPi1IsPR.
apply
 compose1_2IsPR
  with
    (f := fun f : nat => cPairPi2 (A f))
    (f' := fun f : nat =>
           codeSubFormula (cPairPi2 (A f)) (cPairPi1 (A f))
             (codeTerm (Succ (var (cPairPi1 (A f)))))).
apply compose1_1IsPR.
assumption.
apply cPairPi2IsPR.
apply
 compose1_3IsPR
  with
    (f1 := fun f : nat => cPairPi2 (A f))
    (f2 := fun f : nat => cPairPi1 (A f))
    (f3 := fun f : nat => codeTerm (Succ (var (cPairPi1 (A f))))).
apply compose1_1IsPR.
assumption.
apply cPairPi2IsPR.
apply compose1_1IsPR.
assumption.
apply cPairPi1IsPR.
assert
 (isPR 1 (fun f : nat => cPair 3 (S (cPair (cPair 0 (cPairPi1 (A f))) 0)))).
apply
 compose1_2IsPR
  with
    (f := fun f : nat => 3)
    (f' := fun f : nat => S (cPair (cPair 0 (cPairPi1 (A f))) 0)).
apply const1_NIsPR.
apply
 compose1_1IsPR with (f := fun f : nat => cPair (cPair 0 (cPairPi1 (A f))) 0).
apply
 compose1_2IsPR
  with
    (f := fun f : nat => cPair 0 (cPairPi1 (A f)))
    (f' := fun f : nat => 0).
apply
 compose1_2IsPR
  with (f := fun f : nat => 0) (f' := fun f : nat => cPairPi1 (A f)).
apply const1_NIsPR.
apply compose1_1IsPR.
assumption.
apply cPairPi1IsPR.
apply cPairIsPR.
apply const1_NIsPR.
apply cPairIsPR.
apply succIsPR.
apply cPairIsPR.
induction H0 as (x, p).
exists x.
eapply extEqualTrans.
apply p.
simpl in |- *.
intros.
reflexivity.
apply codeSubFormulaIsPR.
apply codeImpIsPR.
apply codeForallIsPR.
apply
 compose1_2IsPR
  with
    (f := fun f : nat => cPairPi1 (A f))
    (f' := fun f : nat => cPairPi2 (A f)).
apply compose1_1IsPR.
assumption.
apply cPairPi1IsPR.
apply compose1_1IsPR.
assumption.
apply cPairPi2IsPR.
apply codeForallIsPR.
apply codeImpIsPR.
apply codeImpIsPR.
apply codeCloseIsPR.
apply idIsPR.
apply eqIsPR.
apply H0.
Qed.

Definition codePA : nat -> bool :=
  orRel 1 (beq_nat (codeFormula PA6))
    (orRel 1 (beq_nat (codeFormula PA5))
       (orRel 1 (beq_nat (codeFormula PA4))
          (orRel 1 (beq_nat (codeFormula PA3))
             (orRel 1 (beq_nat (codeFormula PA2))
                (orRel 1 (beq_nat (codeFormula PA1)) codeInductionSchema))))).

Lemma codePAcorrect1 :
 forall f : Formula,
 codePA (codeFormula f) = true -> mem Formula PA f.
Proof.
intros.
induction (PAdec f).
assumption.
unfold codePA in H.
unfold orRel, nat_rec, nat_rect in H.
unfold PA in |- *.
induction (eq_nat_dec (codeFormula PA6) (codeFormula f)).
rewrite a in H.
rewrite <- beq_nat_refl in H.
replace f with PA6.
right; constructor.
eapply codeFormulaInj.
apply a.
left.
rewrite beq_nat_not_refl in H.
clear b.
induction (eq_nat_dec (codeFormula PA5) (codeFormula f)).
rewrite a in H.
rewrite <- beq_nat_refl in H.
replace f with PA5.
right; constructor.
eapply codeFormulaInj.
apply a.
left.
rewrite beq_nat_not_refl in H.
clear b.
induction (eq_nat_dec (codeFormula PA4) (codeFormula f)).
rewrite a in H.
rewrite <- beq_nat_refl in H.
replace f with PA4.
right; constructor.
eapply codeFormulaInj.
apply a.
left.
rewrite beq_nat_not_refl in H.
clear b.
induction (eq_nat_dec (codeFormula PA3) (codeFormula f)).
rewrite a in H.
rewrite <- beq_nat_refl in H.
replace f with PA3.
right; constructor.
eapply codeFormulaInj.
apply a.
left.
rewrite beq_nat_not_refl in H.
clear b.
induction (eq_nat_dec (codeFormula PA2) (codeFormula f)).
rewrite a in H.
rewrite <- beq_nat_refl in H.
replace f with PA2.
right; constructor.
eapply codeFormulaInj.
apply a.
left.
rewrite beq_nat_not_refl in H.
clear b.
induction (eq_nat_dec (codeFormula PA1) (codeFormula f)).
rewrite a in H.
rewrite <- beq_nat_refl in H.
replace f with PA1.
right; constructor.
eapply codeFormulaInj.
apply a.
left.
rewrite beq_nat_not_refl in H.
apply codeInductionSchemaCorrect2.
simpl in H.
assumption.
assumption.
assumption.
assumption.
assumption.
assumption.
assumption.
Qed.

Lemma codePAcorrect2 :
 forall f : Formula,
 ~ mem Formula PA f -> codePA (codeFormula f) = false.
Proof.
intros.
assert (forall x : bool, x = true \/ x = false).
intros.
induction x; auto.
induction (H0 (codePA (codeFormula f))).
elim H.
apply codePAcorrect1.
assumption.
assumption.
Qed.

Lemma codePAcorrect3 :
 forall f : Formula,
 mem Formula PA f -> codePA (codeFormula f) = true.
Proof.
intros.
unfold codePA in |- *.
unfold orRel, nat_rec, nat_rect in |- *.
do 6 try induction H.
assert (codeInductionSchema (codeFormula x) = true).
apply codeInductionSchemaCorrect1.
apply H.
rewrite H0.
repeat rewrite orb_true_b; repeat rewrite orb_b_true; reflexivity.
induction H.
generalize (codeFormula PA1).
intros.
rewrite <- beq_nat_refl.
repeat rewrite orb_true_b; repeat rewrite orb_b_true; reflexivity.
generalize (codeFormula PA2).
intros.
rewrite <- beq_nat_refl.
repeat rewrite orb_true_b; repeat rewrite orb_b_true; reflexivity.
generalize (codeFormula PA3).
intros.
rewrite <- beq_nat_refl.
repeat rewrite orb_true_b; repeat rewrite orb_b_true; reflexivity.
generalize (codeFormula PA4).
intros.
rewrite <- beq_nat_refl.
repeat rewrite orb_true_b; repeat rewrite orb_b_true; reflexivity.
generalize (codeFormula PA5).
intros.
rewrite <- beq_nat_refl.
repeat rewrite orb_true_b; repeat rewrite orb_b_true; reflexivity.
rewrite <- beq_nat_refl.
repeat rewrite orb_true_b; repeat rewrite orb_b_true; reflexivity.
Qed.

Lemma codePAIsPR : isPRrel 1 codePA.
Proof.
unfold codePA in |- *.
assert (forall n : nat, isPRrel 1 (beq_nat n)).
intros.
apply
 compose1_2IsPR
  with
    (f := fun f : nat => n)
    (f' := fun f : nat => f)
    (g := charFunction 2 beq_nat).
apply const1_NIsPR.
apply idIsPR.
apply eqIsPR.
repeat apply orRelPR; try apply H.
apply codeInductionSchemaIsPR.
Qed.

End Code_PA.

author: princeton-vl

repo: CoqGym

save_path: github-repos/coq/princeton-vl-CoqGym


text:
Require Import Logic.lib.Ensembles_ext.
Require Import Logic.lib.RelationPairs_ext.
Require Import Logic.GeneralLogic.Base.
Require Import Logic.GeneralLogic.ShallowEmbedded.PredicateAsLang.
Require Import Logic.MinimumLogic.Syntax.
Require Import Logic.MinimumLogic.ProofTheory.Minimum.
Require Import Logic.PropositionalLogic.Syntax.
Require Import Logic.PropositionalLogic.ProofTheory.Intuitionistic.
Require Import Logic.PropositionalLogic.ProofTheory.Classical.
Require Import Logic.PropositionalLogic.ShallowEmbedded.PredicatePropositionalLogic.
Require Import Logic.SeparationLogic.Syntax.
Require Import Logic.SeparationLogic.ProofTheory.SeparationLogic.
Require Import Logic.SeparationLogic.ProofTheory.TheoryOfSeparationAxioms.
Require Import Logic.SeparationLogic.Model.SeparationAlgebra.
Require Import Logic.SeparationLogic.Model.OrderedSA.
Require Import Logic.SeparationLogic.Model.OSAGenerators.
Require Import Logic.SeparationLogic.Semantics.WeakSemantics.
Require Import Logic.SeparationLogic.Semantics.StrongSemantics.
Require Import Logic.SeparationLogic.Sound.Sound_Flat.

Instance Pred_sepconL (A: Type) {J: Join A}: SepconLanguage (Pred_L A) :=
  Build_SepconLanguage (Pred_L A) WeakSemantics.sepcon.

Instance Pred_wandL (A: Type) {J: Join A}: WandLanguage (Pred_L A) :=
  Build_WandLanguage (Pred_L A) WeakSemantics.wand.

Instance Pred_empL (A: Type) {J: Join A}: EmpLanguage (Pred_L A) :=
  Build_EmpLanguage (Pred_L A) (@WeakSemantics.emp _ eq J).

Instance Pred_fsepconSM (A: Type) {J: Join A}: @FlatSemantics.SepconSemantics (Pred_L A) (Pred_sepconL A) (Build_Model A) (unit_kMD _) tt eq J (Pred_SM A).
Proof.
  hnf; intros; apply Same_set_refl.
Qed.

Instance Pred_fwandSM (A: Type) {J: Join A}: @FlatSemantics.WandSemantics (Pred_L A) (Pred_wandL A) (Build_Model A) (unit_kMD _) tt eq J (Pred_SM A).
Proof.
  hnf; intros; apply Same_set_refl.
Qed.

Instance Pred_fempSM (A: Type) {J: Join A}: @FlatSemantics.EmpSemantics (Pred_L A) (Pred_empL A) (Build_Model A) (unit_kMD _) tt eq J (Pred_SM A).
Proof.
  apply Same_set_refl.
Qed.

Instance Pred_sepconAX_weak (A: Type) {J: Join A} {SA: SeparationAlgebra A}: SepconAxiomatization_weak (Pred_L A) (Pred_Gamma A).
Proof.
  constructor.
  + intros x y.
    exact (@sound_sepcon_comm (Pred_L A) _ _ (Build_Model A) (unit_kMD _) tt eq J SA (Pred_SM A) (Pred_kminSM A) (Pred_fsepconSM A) x y).
  + intros x y.
    exact (@sound_sepcon_assoc1 (Pred_L A) _ _ (Build_Model A) (unit_kMD _) tt eq J SA (Pred_SM A) (Pred_kminSM A) (Pred_fsepconSM A) x y).
Qed.

Instance Pred_wandAX (A: Type) {J: Join A} {SA: SeparationAlgebra A}: WandAxiomatization (Pred_L A) (Pred_Gamma A).
Proof.
  constructor.
  intros x y z.
  exact (@sound_wand_sepcon_adjoint (Pred_L A) _ _ _ (Build_Model A) (unit_kMD _) tt eq (eq_preorder _) J (Pred_SM A) (Pred_kminSM A) (Pred_fsepconSM A) (Pred_fwandSM A) x y z).
Qed.

Instance Pred_sepconAX (A: Type) {J: Join A} {SA: SeparationAlgebra A}: SepconAxiomatization (Pred_L A) (Pred_Gamma A).
Proof.
  eapply @SepconAxiomatizationWeak2SepconAxiomatization;
  try typeclasses eauto.
  eapply @Adj2SepconMono;
  try typeclasses eauto.
Qed.

Instance Pred_gcsGamma (A: Type) {J: Join A} {SA: SeparationAlgebra A} {incrSA: @IncreasingSeparationAlgebra A eq J}: GarbageCollectSeparationLogic (Pred_L A) (Pred_Gamma A).
Proof.
  intros.
  constructor.
  intros x y.
  exact (@sound_sepcon_elim1 (Pred_L A) _ _ (Build_Model A) (unit_kMD _) tt eq J SA (Pred_SM A) (Pred_kiSM A) (Pred_kminSM A) (Pred_fsepconSM A) incrSA x y).
Qed.

Instance Pred_EmpsGamma (A: Type) {J: Join A} {SA: SeparationAlgebra A} {USA: @UnitalSeparationAlgebra A eq J}: EmpAxiomatization (Pred_L A) (Pred_Gamma A).
Proof.
  constructor.
  + intros x.
    exact (@sound_sepcon_emp1 (Pred_L A) _ _ (Build_Model A) (unit_kMD _) tt eq J SA(Pred_SM A) (Pred_kiSM A) (Pred_kminSM A) (Pred_fsepconSM A) _ (Pred_fempSM A) USA x).
  + intros x.
    exact (@sound_sepcon_emp2 (Pred_L A) _ _ (Build_Model A) (unit_kMD _) tt eq J SA(Pred_SM A) (Pred_kiSM A) (Pred_kminSM A) (Pred_fsepconSM A) _ (Pred_fempSM A) USA x).
Qed.

author: QinxiangCao

repo: UnifySL

save_path: github-repos/coq/QinxiangCao-UnifySL


text:
Require Import CodeDeps.
Require Import Ident.

Local Open Scope Z_scope.

Definition _arg0 := 1%positive.
Definition _arg1 := 2%positive.
Definition _arg2 := 3%positive.
Definition _arg3 := 4%positive.
Definition _function_id := 5%positive.
Definition _i := 6%positive.
Definition _reg := 7%positive.
Definition _ret := 8%positive.
Definition _t'1 := 9%positive.
Definition _t'2 := 10%positive.
Definition _t'3 := 11%positive.
Definition _t'4 := 12%positive.
Definition _t'5 := 13%positive.
Definition _t'6 := 14%positive.

Definition rmm_handler_body :=
  (Ssequence
    (Scall None (Evar _el3_sync_lel (Tfunction Tnil tvoid cc_default)) nil)
    (Ssequence
      (Scall None (Evar _enter_rmm (Tfunction Tnil tvoid cc_default)) nil)
      (Ssequence
        (Ssequence
          (Scall (Some _t'1)
            (Evar _read_reg (Tfunction (Tcons tuint Tnil) tulong cc_default))
            ((Econst_int (Int.repr 0) tuint) :: nil))
          (Sset _function_id (Etempvar _t'1 tulong)))
        (Ssequence
          (Ssequence
            (Scall (Some _t'2)
              (Evar _read_reg (Tfunction (Tcons tuint Tnil) tulong cc_default))
              ((Econst_int (Int.repr 1) tuint) :: nil))
            (Sset _arg0 (Etempvar _t'2 tulong)))
          (Ssequence
            (Ssequence
              (Scall (Some _t'3)
                (Evar _read_reg (Tfunction (Tcons tuint Tnil) tulong
                                  cc_default))
                ((Econst_int (Int.repr 2) tuint) :: nil))
              (Sset _arg1 (Etempvar _t'3 tulong)))
            (Ssequence
              (Ssequence
                (Scall (Some _t'4)
                  (Evar _read_reg (Tfunction (Tcons tuint Tnil) tulong
                                    cc_default))
                  ((Econst_int (Int.repr 3) tuint) :: nil))
                (Sset _arg2 (Etempvar _t'4 tulong)))
              (Ssequence
                (Ssequence
                  (Scall (Some _t'5)
                    (Evar _read_reg (Tfunction (Tcons tuint Tnil) tulong
                                      cc_default))
                    ((Econst_int (Int.repr 4) tuint) :: nil))
                  (Sset _arg3 (Etempvar _t'5 tulong)))
                (Ssequence
                  (Ssequence
                    (Scall (Some _t'6)
                      (Evar _handle_ns_smc (Tfunction
                                             (Tcons tulong
                                               (Tcons tulong
                                                 (Tcons tulong
                                                   (Tcons tulong
                                                     (Tcons tulong Tnil)))))
                                             tulong cc_default))
                      ((Etempvar _function_id tulong) ::
                       (Etempvar _arg0 tulong) :: (Etempvar _arg1 tulong) ::
                       (Etempvar _arg2 tulong) :: (Etempvar _arg3 tulong) ::
                       nil))
                    (Sset _ret (Etempvar _t'6 tulong)))
                  (Sifthenelse (Ebinop One (Etempvar _ret tulong)
                                 (Econst_long (Int64.repr 2) tulong) tint)
                    (Ssequence
                      (Scall None
                        (Evar _exit_rmm (Tfunction (Tcons tulong Tnil) tvoid
                                          cc_default))
                        ((Etempvar _ret tulong) :: nil))
                      (Scall None
                        (Evar _el3_sync_lel (Tfunction Tnil tvoid cc_default))
                        nil))
                    Sskip)))))))))
.

Definition f_rmm_handler := {|
  fn_return := tvoid;
  fn_callconv := cc_default;
  fn_params := nil;
  fn_vars := nil;
  fn_temps := ((_function_id, tulong) :: (_arg0, tulong) ::
               (_arg1, tulong) :: (_arg2, tulong) :: (_arg3, tulong) ::
               (_ret, tulong) :: (_t'6, tulong) :: (_t'5, tulong) ::
               (_t'4, tulong) :: (_t'3, tulong) :: (_t'2, tulong) ::
               (_t'1, tulong) :: nil);
  fn_body := rmm_handler_body
|}.

author: columbia


text:
From Coq Require Import Lists.List.
From Coq Require Import Bool.Bool.
From Coq Require Import Logic.FunctionalExtensionality.
Require Import RBT.Verif.RBtree_Type.
Require Import RBT.Verif.RBtree_Definition.
Require Import RBT.Verif.Half_Tree.
Require Import RBT.Verif.relation_map.
Require Import RBT.Verif.Abstract.

Section Section_SegmentChange.

Class RBtree_with_tag_comm {rbt : RBtree_setting} := {
Optt_comm : forall t1 t2 , Optt t1 t2 = Optt t2 t1
}.

Context {rbt:RBtree_setting}.
Context {rbt_comm : RBtree_with_tag_comm}.
Existing Instance rbt_comm.
Theorem f_twice_comm: forall v t1 t2, f ( f v t1) t2 = f ( f v t2) t1.
Proof.
  intros.
  rewrite f_tag.
  rewrite Optt_comm.
  rewrite f_tag.
  reflexivity.
Qed.
Theorem seg_tag_update : forall  lo hi t t0 m ,
   segment_update lo hi t (tag_update t0 m) =
     tag_update t0 (segment_update lo hi t m).
  Proof.
    intros.
    extensionality x.
    unfold segment_update, tag_update.
    destruct (m x).
    destruct (lo <=? x) ,( x <=? hi).
    simpl. rewrite f_twice_comm. reflexivity.
    simpl. reflexivity.
    simpl. reflexivity.
    simpl. reflexivity.
    reflexivity.
  Qed.

Fixpoint change_segment' (lo hi : Key) (delta: Tag) (s: RBtree) (slo shi: Key) : RBtree :=
if (hi <? lo) then s else (
if (hi <? slo)  || (shi <? lo)
  then s else (
  if (  lo <=? slo ) && ( shi <=? hi) then  tag_tree_t delta s
else
match s with
|Empty => Empty
|T co l k v t r =>  T co (change_segment' lo hi delta l slo k ) k
                     (if (lo <=? k) && (k<=? hi) then f v delta else v) t
                      (change_segment' lo hi delta r k shi)
end
)).

Inductive change_segment lo hi delta s : RBtree -> Prop :=
|seg_intro:  forall low high,  SearchTree' low  s high ->
  change_segment lo hi delta s (change_segment' lo hi delta s low high).

(*Proof *)

    Lemma change_Empty : forall lo hi t slo shi, change_segment' lo hi t Empty slo shi = Empty.
    Proof.
      intros.
      simpl.
      destruct (hi <? lo), ( hi <? slo), (shi <? lo), (lo <=? slo), (shi <=? hi);reflexivity.
    Qed.
    Lemma change_up_defaultmap : forall lo hi t,
        segment_update lo hi t relate_default = relate_default.
    Proof.
      intros. extensionality x.
      unfold segment_update.
      unfold relate_default. reflexivity.
    Qed.
    Lemma change_up_hilo : forall lo hi t m,
      hi < lo ->
        segment_update lo hi t m = m.
    Proof.
      intros. extensionality x.
      unfold segment_update.
      destruct (m x); [| auto].

      remember (lo<=? x) as a.
      remember (x <=? hi) as b.
      destruct a,b;try auto.
      symmetry in Heqa, Heqb.
      solve_order.
    Qed.
    Lemma change_up_notin: forall lo hi m pm t,
     restriction m pm ->
     (forall k, (  lo <= k /\  k <= hi) -> ~ pm k ) ->
       segment_update lo hi t m = m.
    Proof.
      intros. extensionality k.
      pose proof H0 k.
      unfold segment_update.
      unfold restriction in H.
      pose proof H k.
      destruct (m k).
      - remember ( lo <=? k) as u. remember ( k <=? hi) as w. symmetry in Hequ, Heqw.
        destruct u, w.
        assert ( lo <= k /\ k <= hi). { split.  eapply lteb_lte; try eassumption. eapply lteb_lte; try eassumption. }
        exfalso. pose proof H1 H3. apply H4. apply H2. discriminate.
        simpl. reflexivity. reflexivity. reflexivity.
      - reflexivity.
    Qed.
    Lemma change_up_allin: forall lo hi m pm t,
     restriction m pm ->
     (forall k, pm k -> (lo <= k /\  k <= hi)  ) ->
       segment_update lo hi t m = tag_update t m.
    Proof.
      intros. extensionality k.
      pose proof H0 k.
      unfold segment_update , tag_update.
      unfold restriction in H.
      pose proof H k.
      destruct (m k).
      - remember ( lo <=? k) as u. remember ( k <=? hi) as w. symmetry in Hequ, Heqw.
        assert ( lo <= k /\ k <= hi). { apply H1.  apply H2. discriminate. } destruct H3.
        destruct u, w. reflexivity.  solve_order. solve_order. solve_order.
      - reflexivity.
    Qed.

  Theorem segment_st_pre: forall s lo hi t  slo shi, SearchTree' slo s shi ->
     SearchTree' slo (change_segment' lo hi t s slo shi) shi.
  Proof.
    intro.
    induction s.
    + intros.  rewrite change_Empty. auto.
    + intros.
    pose proof search_popro _ _ _ H.
    unfold change_segment'. fold change_segment'.
    inversion H. subst.
    destruct (hi <? lo);[auto |].
    remember ( hi <? slo) as m.
    remember (shi <? lo) as n.
    remember (lo <=? slo) as u.
    remember (shi <=? hi) as w.
    symmetry in Heqm, Heqn, Hequ, Heqw.
    destruct m, n;
   [ simpl; auto| simpl; auto | simpl; auto |  ].
    destruct u ,w;
    [ eapply search_tag_tree_t; try eassumption | | |].
    -
      simpl. apply ST_T. apply IHs1; try eassumption.
      apply IHs2; try eassumption.
    - simpl. apply ST_T. apply IHs1; try eassumption.
      apply IHs2; try eassumption.
    - simpl. apply ST_T. apply IHs1; try eassumption.
      apply IHs2; try eassumption.
  Qed.
  Theorem segement_abs : forall s lo hi t slo shi cts,
   SearchTree' slo s shi -> Abs s cts ->
    Abs (change_segment' lo hi t s slo shi) (segment_update lo hi t cts).
  Proof.
    intro.
    induction s.
    - intros. rewrite change_Empty. inversion H0. subst. rewrite change_up_defaultmap. auto.
    - intros. inversion H. subst.
      unfold change_segment'. fold change_segment'.
      remember (hi<? lo) as a;destruct a.
      --  symmetry in Heqa.
          erewrite change_up_hilo;auto. eapply ltb_lt;auto.
      --
      pose proof restriction_rb _ _ _ _ H H0.
      inversion H0. subst.
      remember ( hi <? slo) as m.
      remember (shi <? lo) as n.
      remember (lo <=? slo) as u.
      remember (shi <=? hi) as w.
      symmetry in Heqm, Heqn, Hequ, Heqw.
      destruct m, n.
      simpl. erewrite change_up_notin; try eassumption. res_intros.
      simpl. erewrite change_up_notin; try eassumption. res_intros.
      simpl. erewrite change_up_notin; try eassumption. res_intros.
      pose proof IHs1 lo hi t0 slo k a H9 H11.
      pose proof IHs2 lo hi t0 k shi b H10 H12.
      assert ( SearchTree' slo (change_segment' lo hi t0 s1 slo k) k). {
      eapply segment_st_pre; try eassumption. }
      assert ( SearchTree' k (change_segment' lo hi t0 s2 k shi) shi). { eapply segment_st_pre; try eassumption . }
      destruct u,w.
      + erewrite change_up_allin;try eassumption.

        eapply tag_tree_abs. auto. intros. super_destruct H6. split. left. tr. left. tr.
      +
        simpl. rewrite seg_tag_update.
      rewrite seg_v_update ; erewrite segment_combine by (first [res_simpl | res_intros ]); eapply Abs_T; try eassumption .
      + rewrite seg_tag_update ;
      rewrite seg_v_update ; erewrite segment_combine by (first [res_simpl | res_intros ]); eapply Abs_T; try eassumption .
      + rewrite seg_tag_update ;
      rewrite seg_v_update ; erewrite segment_combine by (first [res_simpl | res_intros ]); eapply Abs_T; try eassumption .
  Qed.
  Theorem segement_isrb_co : forall s lo hi t slo shi co,
    is_redblack_color s co ->
    SearchTree' slo s shi ->
    is_redblack_color (change_segment' lo hi t s slo shi) co.
  Proof.
    intros.
    revert lo hi t slo shi H0 .
    induction H.
    - intros. rewrite change_Empty. apply IsRB_co_leaf.
    - intros.
      unfold change_segment'. fold change_segment'.
      remember (hi<? lo) as a;destruct a.
      -- eapply IsRB_co_r; auto.
      --
      remember ( hi <? slo) as m.
      remember (shi <? lo) as n.
      destruct m, n.
      eapply IsRB_co_r; try eassumption.
      eapply IsRB_co_r; try eassumption.
      eapply IsRB_co_r; try eassumption.
      inversion H1.
      subst.
      pose proof IHis_redblack_color1 lo hi t slo k H10.
      pose proof IHis_redblack_color2 lo hi t k shi H11.
      destruct (lo <=? slo), (shi <=? hi).
      eapply isrb_tagupdate. eapply IsRB_co_r; try eassumption.
      eapply IsRB_co_r; try eassumption.
      eapply IsRB_co_r; try eassumption.
      eapply IsRB_co_r; try eassumption.
    - intros.
      unfold change_segment'. fold change_segment'.
      remember (hi<? lo) as a;destruct a.
      -- eapply IsRB_co_b; auto.
      --
      remember ( hi <? slo) as m.
      remember (shi <? lo) as n.
      destruct m, n.
      eapply IsRB_co_b; try eassumption.
      eapply IsRB_co_b; try eassumption.
      eapply IsRB_co_b; try eassumption.
      inversion H1.
      subst.
      pose proof IHis_redblack_color1 lo hi t slo k H10.
      pose proof IHis_redblack_color2 lo hi t k shi H11.
      destruct (lo <=? slo), (shi <=? hi).
      eapply isrb_tagupdate. eapply IsRB_co_b; try eassumption.
      eapply IsRB_co_b; try eassumption.
      eapply IsRB_co_b; try eassumption.
      eapply IsRB_co_b; try eassumption.
  Qed.
  Theorem segement_isrb_dep: forall s lo hi t slo shi n,
    is_redblack_dep s n ->
    SearchTree' slo s shi ->
    is_redblack_dep (change_segment' lo hi t s slo shi) n.
  Proof.
    intros.
    revert lo hi t slo shi H0 .
    induction H.
    - intros. rewrite change_Empty. apply IsRB_dep_em.
    - intros.
      unfold change_segment'. fold change_segment'.
      remember (hi<? lo) as a;destruct a;[eapply IsRB_dep_r;auto |].
      destruct ( hi <? slo), (shi <? lo).
      eapply IsRB_dep_r; try eassumption.
      eapply IsRB_dep_r; try eassumption.
      eapply IsRB_dep_r; try eassumption.
      inversion H1.
      subst.
      pose proof IHis_redblack_dep1 lo hi t slo k H10.
      pose proof IHis_redblack_dep2 lo hi t k shi H11.
      destruct (lo <=? slo), (shi <=? hi).
      eapply isrb_tagupdate_dep. eapply IsRB_dep_r; try eassumption.
      eapply IsRB_dep_r; try eassumption.
      eapply IsRB_dep_r; try eassumption.
      eapply IsRB_dep_r; try eassumption.
    - intros.
      unfold change_segment'. fold change_segment'.
      remember (hi<? lo) as a;destruct a;[eapply IsRB_dep_b;auto | ].
      destruct ( hi <? slo), (shi <? lo).
      eapply IsRB_dep_b; try eassumption.
      eapply IsRB_dep_b; try eassumption.
      eapply IsRB_dep_b; try eassumption.
      inversion H1.
      subst.
      pose proof IHis_redblack_dep1 lo hi t slo k H10.
      pose proof IHis_redblack_dep2 lo hi t k shi H11.
      destruct (lo <=? slo), (shi <=? hi).
      eapply isrb_tagupdate_dep. eapply IsRB_dep_b; try eassumption.
      eapply IsRB_dep_b; try eassumption.
      eapply IsRB_dep_b; try eassumption.
      eapply IsRB_dep_b; try eassumption.
  Qed.

Theorem segement_keep: forall s lo hi t tree, SearchTree s -> is_redblack s ->
 change_segment lo hi t s tree ->
 SearchTree tree /\  is_redblack tree .
Proof.
  intros.
  inversion H. subst.
  destruct H0.
  destruct H3.
  inversion H1. subst.

  split.
  eapply ST_intro .
  eapply (segment_st_pre s lo hi t); try eassumption.
  split.
  eapply segement_isrb_co; try eassumption.
  exists x.
  eapply segement_isrb_dep; try eassumption.
Qed.

End Section_SegmentChange.

author: maoliyuan

repo: avltree-verification


text:
Require Import Iron.Language.SystemF2Effect.Value.Relation.TyJudge.

(* Weakening Type Env in Type Judgement.
   We can insert a new type into the type environment, provided we
   lift existing references to types higher in the stack across
   the new one. *)
Lemma type_tyenv_insert
 :  forall ke te se sp ix x t1 e1 t2
 ,  TypeX  ke te se sp x t1 e1
 -> TypeX  ke (insert ix t2 te) se sp (liftXX 1 ix x) t1 e1.
Proof.
 intros. gen ix ke se sp te t1 e1 t2.
 induction x using exp_mutind with
  (PV := fun v => forall ix ke se sp te t1 t2
      ,  TypeV ke te se sp v t1
      -> TypeV ke (insert ix t2 te) se sp (liftXV 1 ix v) t1)
  ; intros; inverts_type; simpl; eauto.

 - Case "VVar".
   nnat; lift_cases; burn.

 - Case "VLam".
   apply TvLam; eauto.
   rewrite insert_rewind. auto.

 - Case "VLAM".
   apply TvLAM.
   have ( liftTE 0 (insert ix t2 te)
        = insert ix (liftTT 1 0 t2) (liftTE 0 te))
    by (unfold liftTE; rewrite map_insert; auto).
   rewritess. eauto.

 - Case "XLet".
   apply TxLet; eauto.
   rewrite insert_rewind. eauto.

 - Case "XPrivate".
   eapply TxPrivate with (t := t) (e := e); eauto.
   have ( liftTE 0 (insert ix t2 te)
        = insert ix (liftTT 1 0 t2) (liftTE 0 te))
    by (unfold liftTE; rewrite map_insert; auto).
   rewritess. eauto.

 - Case "XExtend".
   eapply TxExtend; eauto.
   have ( liftTE 0 (insert ix t2 te)
        = insert ix (liftTT 1 0 t2) (liftTE 0 te))
    by (unfold liftTE; rewrite map_insert; auto).
   rewritess. eauto.
Qed.

(* We can push a new type onto the environment stack provided
   we lift references to existing types across the new one. *)
Lemma type_tyenv_weaken1
 :  forall ke te se sp x t1 e1 t2
 ,  TypeX  ke te se sp x t1 e1
 -> TypeX  ke (te :> t2) se sp (liftXX 1 0 x) t1 e1.
Proof.
 intros.
 rrwrite (te :> t2 = insert 0 t2 te).
 burn using type_tyenv_insert.
Qed.

(* We can push a new type into the enviroment of a type-of-value
   judgement provided we lift references to existing types across
   the new one *)
Lemma typev_tyenv_weaken1
 :  forall ke te se sp v t1 t2
 ,  TypeV  ke te se sp v t1
 -> TypeV  ke (te :> t2) se sp (liftXV 1 0 v) t1.
Proof.
 intros.
 have HX: (TypeX ke te se sp (XVal v) t1 (TBot KEffect)).
 eapply type_tyenv_weaken1 in HX.
 simpl in HX. inverts HX. eauto.
Qed.

(* We can several new types onto the environment stack provided
   we lift referenes to existing types across the new one. *)
Lemma type_tyenv_weaken_append
 :  forall ke te se sp te' x t1 e1
 ,  TypeX  ke te se sp x t1 e1
 -> TypeX  ke (te >< te') se sp (liftXX (length te') 0 x) t1 e1.
Proof.
 intros.
 induction te'; simpl.
  - burn.

  - rrwrite (S (length te') = length te' + 1).
    rrwrite (length te' + 1 = 1 + length te').
    rewrite <- liftXX_plus.
    eapply type_tyenv_weaken1.
    burn.
Qed.

author: DonaldKellett

repo: iron-lambda


text:
(** Exercise sheet for lecture 4: Tactics in Coq.

This is the material for the advisors with solutions.

Written by Ralph Matthes (CNRS, IRIT, Univ. Toulouse, France).
*)

(** * Exercise 1
Formalize the solutions of exercise 1 of Lecture 1.

[[
For each of the following types, write down an element of that type, if it has one. If it does not have any elements, you should establish that this is the case. But first think how this can be done in type theory! It ought to be just another construction.

1.    A × (B + C) → A × B + A × C, given types A, B, C
2.    (A → A) → (A → A), given type A (for extra credit, write down five elements of this type)
3.    Id_nat (0, succ 0)
4.    ∑ (A : Universe) (A → empty) → empty
5.    ∏ (n : nat), ∑ (m : nat), Id_nat n (2 * m) + Id_nat n (2 * m + 1), assuming you have got arithmetic
6.    (∑ (x : A) B × P x) → B × ∑ (x : A) P x, given types A, B, and P : A → Universe
7.    B → (B → A) → A, given types A and B
8.    B → ∏ (A : Universe) (B → A) → A, given type B
9.    (∏ (A : Universe) (B → A) → A) → B, given type B
]]

For the present exercise, this means: state the formula as a lemma, give a proof interactively if there is a proof, and give a counter-example otherwise, i.e., give specific parameters and a proof of the negation of the statement.

More precise instructions and hints:

1. Use [⨿] in place of the + and pay attention to operator precedence.

2. Write a function that provides different elements for any natural number argument, not just five elements; for extra credits: state correctly that they are different - for a good choice of [A]; for more extra credits: prove that they are different.

3. An auxiliary function may be helpful - better recall the trick.

4. The symbol for Sigma-types is [∑], not [Σ].

5. Same as 1; and there is need for module [UniMath.Foundations.NaturalNumbers], e.g., for Lemma [natpluscomm].

6.-9. no further particulars
*)

Require Import UniMath.Foundations.Preamble.
Require Import UniMath.Foundations.PartA.

Lemma Exo1_1 (A B C: UU): A × (B ⨿ C) → (A × B) ⨿ (A × C).
Proof.
  intro H123.
  induction H123 as [H1 H23].
  induction H23 as [H2 | H3].
  - apply ii1.
    apply make_dirprod.
    + exact H1.
    + exact H2.
  - apply ii2.
    apply make_dirprod.
    + exact H1.
    + exact H3.
Defined.

Lemma Exo1_2 (A: UU)(n: nat): (A → A) → (A → A).
Proof.
  intros f a.
  induction n as [| _ IH].
  - exact a.
  - exact (f IH).
Defined.

(** of course, the iterator of lecture 2 could be used here *)

Lemma Exo1_2_bonus (n1 n2: nat): ¬ (n1 = n2) -> ¬ (Exo1_2 nat n1 = Exo1_2 nat n2).
Proof.
  intros Hypn Hyp.
  assert (H1: Exo1_2 nat n1 S 0 = Exo1_2 nat n2 S 0).
  { rewrite Hyp.
    apply idpath.
  }
  assert (H2: ∏ n:nat, Exo1_2 nat n S 0 = n).
  { induction n.
    - apply idpath.
    - cbn.
      apply maponpaths.
      exact IHn.
  }
  rewrite H2 in H1.
  rewrite H2 in H1.
  apply Hypn.
  exact H1.
Defined.

(** counter-example needed - this is difficult to invent *)
Lemma Exo1_3: ¬ (0 = S 0).
Proof.
  intro H.
  apply nopathstruetofalse.
  set (aux := nat_rect (λ _ : nat, bool) true (λ _ _, false)).
  assert (H1: aux 0 = aux 1).
  { rewrite <- H.
    reflexivity.
  }
  cbn in H1.
  exact H1.
Defined.

Lemma Exo1_4: ∑ (A: UU), ( A -> ∅ ) -> ∅.
Proof.
  use tpair.
  - exact unit.
  - cbn.
    intro H.
    apply H.
    exact tt.
Defined.

Require Import UniMath.Foundations.NaturalNumbers.

Lemma Exo1_5 (n: nat): ∑ m:nat, (n = 2 * m) ⨿ (n = 2 * m + 1).
Proof.
  induction n as [| n IHn].
  - exists 0.
    apply ii1.
    apply idpath.
  - induction IHn as [m H].
    induction H as [H1 | H2].
    + exists m.
      apply ii2.
      rewrite H1.
      rewrite natpluscomm.
      apply idpath.
    + exists (S m).
      apply ii1.
      rewrite H2.
      rewrite natpluscomm.
      rewrite natmultcomm.
      cbn.
      rewrite natpluscomm.
      cbn.
      rewrite natmultcomm.
      apply idpath.
Defined.

Lemma Exo1_6 (A B: UU)(P: A -> UU): (∑ (x : A), B × P x) → B × ∑ (x : A), P x.
Proof.
  intro H.
  induction H as [x H12].
  induction H12 as [H1 H2].
  apply make_dirprod.
  - exact H1.
  - exists x.
    exact H2.
Defined.

Lemma Exo1_7 (A B: UU): B → (B → A) → A.
Proof.
  intros b f.
  exact (f b).
Defined.

Lemma Exo1_8 (B: UU): B → ∏ (A : UU), (B → A) → A.
Proof.
  intros b ? f.
  exact (f b).
Defined.

Lemma Exo1_9 (B: UU): (∏ (A : UU), (B → A) → A) → B.
Proof.
  intro H.
  apply H.
  intro b.
  exact b.
Defined.

(** * Exercise 2
Define two computable strict comparison operators for natural numbers based on the fact
that [m < n] iff [n - m <> 0] iff [(m+1) - n = 0]. Prove that the two operators are
equal (using function extensionality, i.e., [funextfunStatement] in the UniMath library).

It may be helpful to use the definitions of the exercises for lecture 2.
The following lemmas on substraction [sub] in the natural numbers may be
useful:

a) [sub n (S m) = pred (sub n m)]

b) [sub 0 n = 0]

c) [pred (sub 1 n) = 0]

d) [sub (S n) (S m) = sub n m]

*)

(** from exercises to Lecture 2: *)
Definition ifbool (A : UU) (x y : A) : bool -> A :=
  bool_rect (λ _ : bool, A) x y.

Definition negbool : bool -> bool := ifbool bool false true.

Definition nat_rec (A : UU) (a : A) (f : nat -> A -> A) : nat -> A :=
  nat_rect (λ _ : nat, A) a f.

Definition pred : nat -> nat := nat_rec nat 0 (fun x _ => x).

Definition is_zero : nat -> bool := nat_rec bool true (λ _ _, false).

Definition iter (A : UU) (a : A) (f : A → A) : nat → A :=
  nat_rec A a (λ _ y, f y).

Notation "f ̂ n" := (λ x, iter _ x f n) (at level 10).

Definition sub (m n : nat) : nat := pred ̂ n m.

(** new material: *)

Definition ltnat1 (m n : nat) : bool := is_zero (sub (S m) n).
Definition ltnat2 (m n : nat) : bool := negbool (is_zero (sub n m)).

(** the helper lemmas : *)
Lemma Exo2_aux1 (n m: nat) : sub n (S m) = pred (sub n m).
Proof.
  apply idpath.
Defined.

Lemma Exo2_aux2 (n: nat) : sub 0 n = 0.
Proof.
  induction n as [| n IHn].
  + apply idpath.
  + cbn.
    change (iter nat 0 pred n) with (sub 0 n).
    rewrite IHn.
    apply idpath.
Defined.

Lemma Exo2_aux3 (n: nat) : pred (sub 1 n) = 0.
Proof.
  induction n as [| n IHn].
  + cbn.
    apply idpath.
  + cbn.
    fold (sub 1 n).
    rewrite IHn.
    cbn.
    apply idpath.
Defined.

Lemma Exo2_aux4 (n m: nat) : sub (S n) (S m) = sub n m.
Proof.
  induction m as [| m IHm].
  - apply idpath.
  - rewrite (Exo2_aux1 (S n) (S m)).
    rewrite (Exo2_aux1 n m).
    apply maponpaths.
    exact IHm.
Defined.

(** the exercise itself: *)
Lemma Exo2: ltnat1 = ltnat2.
Proof.
  apply funextfun.
  intro m.
  induction m as [| m IHm].
  - apply funextfun.
    intro n.
    induction n as [| n IHn].
    + apply idpath.
    + cbn.
      fold (sub 1 n).
      rewrite Exo2_aux3.
      apply idpath.
  - apply funextfun.
    intro n.
    induction n as [ | n1 IHn1].
    + cbn.
      unfold ltnat2.
      rewrite Exo2_aux2.
      apply idpath.
    + unfold ltnat1, ltnat2.
      rewrite Exo2_aux4.
      rewrite Exo2_aux4.
      change (ltnat1 m n1 = ltnat2 m n1).
      rewrite IHm.
      apply idpath.
Defined.

author: UniMath

repo: Schools

save_path: github-repos/coq/UniMath-Schools


text:
Require Import Coq.Unicode.Utf8.

Module NatPlayground.

  Inductive nat : Type :=
  | O : nat
  | S : nat → nat.

  Definition pred (n : nat) : nat :=
    match n with
    | O => O
    | (S k) => k
    end.

  Check (S (S (S O))).

  Fixpoint plus (x y : nat) : nat :=
    match x with
    | O => y
    | (S k) => (S (plus k y))
    end.

  Compute plus (S (S O)) (S (S (S O))).

  Fixpoint mult (x y : nat) : nat :=
    match x with
    | O => O
    | (S k) => plus y (mult k y)
    end.

  Compute mult (S (S (S O))) (S (S O)).

  Example test_mult : (mult (S (S (S O))) (S (S (S O))))
                       = (S (S (S (S (S (S (S (S (S O))))))))).
  Proof. simpl. reflexivity. Qed.

  Fixpoint minus (x y : nat) : nat :=
    match (x, y) with
    | (O, _) => O
    | (S _, O) => x
    | (S n, S k) => minus n k
    end.

  Notation "x + y" := (plus x y) (at level 50, left associativity) .

  Notation "x - y" := (minus x y) (at level 50, left associativity).

  Notation "x × y" := (mult x y) (at level 40, left associativity).

  Compute (S (S O)) + (S (S O)) × (S (S O)).

End NatPlayground.

Check (S (S (S O))).

Definition minustwo (n : nat) : nat :=
  match n with
  | O => O
  | (S O) => O
  | (S (S k)) => k
  end.

Compute (minustwo 4).

Fixpoint evenb (n : nat) : bool :=
  match n with
  | O => true
  | (S O) => false
  | (S (S k)) => evenb k
  end.

Definition oddb (n : nat) : bool :=
  negb (evenb n).

Example test_oddb1 : oddb 1 = true.
Proof. simpl. reflexivity. Qed.

Example test_oddb2: oddb 4 = false.
Proof. simpl. reflexivity. Qed.

Check mult.

(* Ex 1 *)
Fixpoint factorial (n : nat) : nat :=
  match n with
  | O => O
  | (S O) => (S O)
  | (S k) => mult n (factorial k)
  end.

Example test_factorial1: (factorial 3) = 6.
Proof. simpl. reflexivity. Qed.

Example test_factorial2: (factorial 5) = (mult 10 12).
Proof. simpl. reflexivity. Qed.

(* Ex2 *)

(* Потом сделаю, лучше буду прувить *)

Theorem plus_O_n : ∀ n : nat, 0 + n = n.
Proof.
  intros n.
  reflexivity.
Qed.

Theorem mult_0_l : ∀  n : nat, 0 * n = 0.
Proof.
  intros n.
  reflexivity.
Qed.

Theorem plus_id_example : ∀ n m : nat, n = m → n + n = m + m.
Proof.
  intros n m.
  intros H.
  rewrite -> H.
  reflexivity.
Qed.

(* Ex 3 *)
Theorem plus_id_exercise : ∀ n m o : nat, n = m → m = o -> n + m = m + o.
Proof.
  intros n m o.
  intros H.
  intros J.
  rewrite -> H.
  rewrite <- J.
  reflexivity.
Qed.

Theorem mult_0_plus : ∀ n m : nat, (0 + n) * m = n * m.
Proof.
  intros n m.
  rewrite -> plus_O_n.
  reflexivity.
Qed.

Theorem plus_1_S_n : ∀ n : nat, 1 + n = S n.
Proof.
  intros n.
  reflexivity.
Qed.

(* Ex 4 *)
Theorem mult_S_1 : ∀ n m : nat, m = S n → m * (1 + n) = m * m.
Proof.
  intros n m.
  intros H.
  rewrite -> plus_1_S_n.
  rewrite <- H.
  reflexivity.
Qed.

Fixpoint beq_nat (n m : nat) : bool :=
  match n with
  | O => match m with
         | O => true
         | S m' => false
         end
  | S n' => match m with
            | O => false
            | S m' => beq_nat n' m'
            end
  end.

Theorem plus_1_neq_0_firsttry : ∀ n : nat, beq_nat (n + 1) 0 = false.
Proof.
  intros n.
  destruct n as [| n'].
  - reflexivity.
  - reflexivity.
Qed.

Theorem negb_involutive : forall b : bool, negb (negb b) = b.
Proof.
  intros b.
  destruct b.
  - reflexivity.
  - reflexivity.
Qed.

Theorem andb_commutative : forall b c, andb b c = andb c b.
Proof.
  intros b c.
  destruct b.
  - destruct c.
    + reflexivity.
    + reflexivity.
  - destruct c.
    + reflexivity.
    + reflexivity.
Qed.

(*

∧-commutative : ∀ (b c : 𝔹) -> (b ∧ c) ≡ (c ∧ b)
∧-commutative tt tt = refl
∧-commutative tt ff = refl
∧-commutative ff tt = refl
∧-commutative ff ff = refl

 *)

Theorem plus_1_neq_0' : ∀ n : nat, beq_nat (n + 1) 0 = false.
Proof.
  intros [|n].
  - reflexivity.
  - reflexivity.
Qed.

Theorem andb_commutative'' : ∀ b c, andb b c = andb c b.
Proof.
  intros [] [].
  - reflexivity.
  - reflexivity.
  - reflexivity.
  - reflexivity.
Qed.

(*
∧-true-elim : ∀ (b c : 𝔹) → (b ∧ c) ≡ tt → c ≡ tt
∧-true-elim tt c p = p -- Hm~
∧-true-elim ff tt p = refl
∧-true-elim ff ff ()
*)

Theorem andb_true_elim2 : ∀ b c : bool, andb b c = true → c = true.
Proof.
  intros b c.
  intros H.
  destruct c.
  - reflexivity.
  - rewrite <- H.
    destruct b.
    + reflexivity.
    + reflexivity.
Qed.

Theorem zero_nbeq_plus_1 : ∀ n : nat, beq_nat 0 (n + 1) = false.
Proof.
  intros [|n].
  - reflexivity.
  - reflexivity.
Qed.

(* Ex *)

Theorem identity_fn_applied_twice :
  ∀ (f : bool → bool), (∀ (x : bool), f x = x) → ∀ (b : bool), f (f b) = b.
Proof.
  intros f x b.
  rewrite -> x.
  rewrite -> x.
  reflexivity.
Qed.

Theorem negation_fn_applied_twice :
  ∀ (f : bool → bool), (∀ (x : bool), f x = negb x) → ∀ (b : bool), f (f b) = b.
Proof.
  intros f x b.
  rewrite -> x.
  rewrite -> x.
  destruct b.
  - reflexivity.
  - reflexivity.
Qed.

(*
∧-eq-∨ : ∀ (b c : 𝔹) -> (b ∧ c) ≡ (b ∨ c) → b ≡ c
∧-eq-∨ tt .tt refl = refl
∧-eq-∨ ff tt ()
∧-eq-∨ ff ff refl = refl
*)

(*
Theorem andb_eq_orb : ∀ (b c : bool), (andb b c = orb b c) → b = c.
Proof.
  intros b c H. (* TODO *)
 *)

(* Ex *)
Inductive bin : Type :=
| BO : bin (* 0 *)
| BS : bin -> bin (* 1 + n *)
| BTwice : bin -> bin. (* 2 × n *)

(*
TODO
Спорно. Надо переделать.
Definition incr (n : bin) : bin :=
  match n with
  | BO => BS BO (* 0 + 1 *)
  | (BS BO) => (BS (BS BO)) (* ≠ 2 * 0, 1 + 1 + 0 *)
  | (BS k) => BTwice k (* косяк *)
  | (BTwice k) => BS (BTwice k)
  end.

Fixpoint bin_to_nat (b : bin) : nat :=
  match b with
  | BO => 0
  | (BS k) => 1 + (bin_to_nat k)
  | (BTwice k) => 2 * (bin_to_nat k)
  end.

Compute (BTwice (BS (BTwice (BS BO)))).

(* Test with zero *)

Example test_bin_incr1 :
  bin_to_nat (incr (incr (BTwice (BTwice (BS BO))))) = 6.
Proof.
  simpl.
  reflexivity.
Qed.

Example test_bin_incr2 : (incr (incr (incr (incr BO)))) = (BTwice ().
Proof.
  reflexivity.
Qed.
*)

author: Fwerskaje

repo: notes-on-functional-programming


text:
Require Import Coq.Program.Equality.
Require Import Coq.Sets.Ensembles.
Require Import Omega.

Add LoadPath "." as Top0.
Require Import Top0.Tactics.
Require Import Top0.Keys.
Require Import Top0.Nameless.
Require Import Top0.Definitions.
Require Import Top0.Axioms.

Lemma subst_rho_natural :
  forall rho, subst_rho rho Ty2_Natural = Ty2_Natural.
Proof.
  unfold subst_rho. unfold R.fold. unfold R.Raw.fold.
  intro rho. destruct rho. simpl. induction this.
  - reflexivity.
  - inversion is_bst; subst.
    rewrite IHthis1 by assumption.
    replace (subst_in_type k e Ty2_Natural) with Ty2_Natural.
    rewrite IHthis2 by assumption.
    reflexivity.
    unfold subst_in_type, open_var, close_var.
    simpl. reflexivity.
Qed.

Lemma subst_rho_boolean :
  forall rho, subst_rho rho Ty2_Boolean = Ty2_Boolean.
Proof.
  unfold subst_rho. unfold R.fold. unfold R.Raw.fold.
  intro rho. destruct rho. simpl. induction this.
  - reflexivity.
  - inversion is_bst; subst.
    rewrite IHthis1 by assumption.
    replace (subst_in_type k e Ty2_Boolean) with Ty2_Boolean.
    rewrite IHthis2 by assumption.
    reflexivity.
    unfold subst_in_type, open_var, close_var.
    simpl. reflexivity.
Qed.

Lemma subst_rho_unit :
  forall rho, subst_rho rho Ty2_Unit = Ty2_Unit.
Proof.
  unfold subst_rho. unfold R.fold. unfold R.Raw.fold.
  intro rho. destruct rho. simpl. induction this.
  - reflexivity.
  - inversion is_bst; subst.
    rewrite IHthis1 by assumption.
    replace (subst_in_type k e  Ty2_Unit) with  Ty2_Unit.
    rewrite IHthis2 by assumption.
    reflexivity.
    unfold subst_in_type, open_var, close_var.
    simpl. reflexivity.
Qed.

Lemma subst_rho_effect :
  forall rho, subst_rho rho Ty2_Effect = Ty2_Effect.
Proof.
  unfold subst_rho. unfold R.fold. unfold R.Raw.fold.
  intro rho. destruct rho. simpl. induction this.
  - reflexivity.
  - inversion is_bst; subst.
    rewrite IHthis1 by assumption.
    replace (subst_in_type k e  Ty2_Effect) with  Ty2_Effect.
    rewrite IHthis2 by assumption.
    reflexivity.
    unfold subst_in_type, open_var, close_var.
    simpl. reflexivity.
Qed.

Lemma subst_rho_rgn_const :
  forall rho c, fold_subst_rgn rho (Rgn2_Const true true c) = (Rgn2_Const true true c).
Proof.
  intros rho c.
  unfold  fold_subst_rgn. unfold R.fold. unfold R.Raw.fold.
  destruct rho. simpl. induction this.
  - reflexivity.
  - inversion is_bst; subst.
    rewrite IHthis1 by assumption.
    replace (subst_rgn k (Rgn2_Const true false e) (Rgn2_Const true true c)) with (Rgn2_Const true true c).
    rewrite IHthis2 by assumption.
    reflexivity.
    simpl. reflexivity.
Qed.

Lemma subst_rho_index :
  forall rho n, fold_subst_rgn rho (Rgn2_BVar true true n) = (Rgn2_BVar true true n).
Proof.
  intros rho n.
  unfold  fold_subst_rgn. unfold R.fold. unfold R.Raw.fold.
  destruct rho. simpl. induction this.
  - reflexivity.
  - inversion is_bst; subst.
    rewrite IHthis1 by assumption.
    replace (subst_rgn k (Rgn2_Const true false e) (Rgn2_BVar true true n)) with (Rgn2_BVar true true n).
    rewrite IHthis2 by assumption.
    reflexivity.
    simpl. reflexivity.
Qed.

Lemma fold_eps_leaf :
forall eff is_bst,
  eff = (fun sa : StaticAction2 =>
           exists sa' : StaticAction2, eff sa' /\
                                       fold_subst_sa {| R.this := R.Raw.Leaf Region; R.is_bst := is_bst |} sa' = sa).
Proof.
 intros eff is_bst.
 apply Extensionality_Ensembles;
      unfold Same_set, Included; split; intros x H.
      * unfold In in *.
        exists x. intuition. unfold fold_subst_sa. destruct x; unfold fold_subst_rgn, subst_rgn; f_equal.
      * unfold In in *.  destruct H as [sa [? ?]].
        assert ( fold_subst_sa {| R.this := R.Raw.Leaf Region; R.is_bst := is_bst |} sa = sa)
          by (unfold fold_subst_sa, fold_subst_rgn, subst_rgn; simpl; destruct sa; subst; f_equal).
        rewrite H1 in H0. now subst.
Qed.

Lemma fold_eps_node :
  forall eff k t e this1 this2
         (Hl : R.Raw.bst this1)
         (Hr : R.Raw.bst this2)
         (is_bst : R.Raw.bst (R.Raw.Node this1 k e this2 t)),
    fold_subst_eps {| R.this := this2; R.is_bst := Hr |}
     (subst_eps k (Rgn2_Const true false e)
        (fold_subst_eps {| R.this := this1; R.is_bst := Hl |} eff)) =
   fold_subst_eps
     {| R.this := R.Raw.Node this1 k e this2 t; R.is_bst := is_bst |} eff.
Proof.
  intros eff k t e this1 this2 Hl Hr is_bst.
  apply Extensionality_Ensembles;
  unfold Same_set, Included; split; intros x H; unfold In in *.
  - unfold fold_subst_eps in *.
    destruct H as [sa [[sa' [[sa'' [H1 H2]] H3]] H4]].
    exists sa''. intuition. subst.
    unfold fold_subst_sa, subst_sa; destruct sa''; f_equal.
  - unfold fold_subst_eps in *.
    destruct H as [sa [H1 H2]].
    exists (subst_sa k (Rgn2_Const true false e) (fold_subst_sa {| R.this := this1; R.is_bst := Hl |} sa)).
    split.
    + unfold subst_eps.
      exists (fold_subst_sa {| R.this := this1; R.is_bst := Hl |} sa).
      intuition. exists sa. intuition.
    + destruct sa; rewrite <- H2; simpl; f_equal.
Qed.

Lemma subst_rho_pair :
  forall rho t1 t2,
    subst_rho rho (Ty2_Pair t1 t2) = Ty2_Pair (subst_rho rho t1) (subst_rho rho t2).
Proof.
  unfold subst_rho.
  unfold R.fold. unfold R.Raw.fold.
  intro rho. destruct rho. simpl. induction this; intros t1 t2.
  - reflexivity.
  - assert (Hl: R.Raw.bst this1) by (inversion is_bst; auto).
    assert (Hr: R.Raw.bst this2) by (inversion is_bst; auto).
    rewrite IHthis1 by assumption. f_equal.
    unfold subst_in_type; simpl.
    rewrite IHthis2 by assumption. f_equal.
Qed.

Lemma subst_rho_arrow :
  forall rho tyr1 eff1 tyr2 eff2 tyr3,
    subst_rho rho (Ty2_Arrow tyr1 eff1 tyr2 eff2 tyr3) = Ty2_Arrow (subst_rho rho tyr1) (fold_subst_eps rho eff1) (subst_rho rho tyr2)
                                                                   (fold_subst_eps rho eff2) (subst_rho rho tyr3) .
Proof.
  unfold subst_rho.
  unfold R.fold. unfold R.Raw.fold.
  intro rho. destruct rho. simpl. induction this; intros tyr1 eff1 tyr2 eff2 tyr3.
  - f_equal; unfold fold_subst_eps; apply fold_eps_leaf.
  - assert (Hl: R.Raw.bst this1) by (inversion is_bst; auto).
    assert (Hr: R.Raw.bst this2) by (inversion is_bst; auto).
    rewrite IHthis1 with (is_bst:=Hl) by assumption. f_equal.
    unfold subst_in_type; simpl.
    rewrite IHthis2 with (is_bst:=Hr) by assumption. f_equal.
    + apply fold_eps_node.
    + apply fold_eps_node.
Qed.

Lemma subst_rho_tyref : forall rho r ty,subst_rho rho (Ty2_Ref r ty) =  Ty2_Ref (fold_subst_rgn rho r) (subst_rho rho ty).
Proof.
  unfold subst_rho, fold_subst_rgn. unfold R.fold. unfold R.Raw.fold.
  intro rho. destruct rho. simpl. induction this; intros r ty.
  - reflexivity.
  - inversion is_bst; subst.
    rewrite IHthis1 by assumption.
    unfold subst_in_type, open_var, close_var; simpl.
    rewrite IHthis2 by assumption.
    unfold subst_in_type, open_var, close_var. simpl.
    reflexivity.
Qed.

Lemma subst_rho_forallrgn  :
  forall rho eff rty,
    subst_rho rho (Ty2_ForallRgn eff rty) = Ty2_ForallRgn (fold_subst_eps rho eff) (subst_rho rho rty).
Proof.
  unfold subst_rho, fold_subst_eps. unfold R.fold. unfold R.Raw.fold.
  intro rho. destruct rho. simpl. induction this; intros eff rty.
  - f_equal; unfold fold_subst_eps; apply fold_eps_leaf.
  - assert (Hl: R.Raw.bst this1) by (inversion is_bst; auto).
    assert (Hr: R.Raw.bst this2) by (inversion is_bst; auto).
    rewrite IHthis1 with (is_bst:=Hl) by assumption. f_equal.
    unfold subst_in_type; simpl.
    rewrite IHthis2 with (is_bst:=Hr) by assumption. f_equal.
    apply fold_eps_node.
Qed.

Lemma subst_rho_fvar_1:
  forall rho x,
    (exists v, fold_subst_rgn rho (Rgn2_FVar true true x) = Rgn2_Const true true v) \/
    fold_subst_rgn rho (Rgn2_FVar true true x) = Rgn2_FVar true true x.
Proof.
  intro rho. destruct rho. induction this; intros x.
  - unfold fold_subst_rgn, R.fold, R.Raw.fold; simpl. right. reflexivity.
  - assert (Hl: R.Raw.bst this1) by (inversion is_bst; auto).
    assert (Hr: R.Raw.bst this2) by (inversion is_bst; auto).
    replace (fold_subst_rgn {| R.this := R.Raw.Node this1 k e this2 t; R.is_bst := is_bst |} (Rgn2_FVar true true x))
    with
    (fold_subst_rgn {| R.this := this2; R.is_bst := Hr |}
                    (subst_rgn k (Rgn2_Const true false e)
                               (fold_subst_rgn {| R.this := this1; R.is_bst := Hl |} (Rgn2_FVar true true x)))
    ) by (unfold fold_subst_rgn, R.fold, R.Raw.fold in *; reflexivity).
    destruct (IHthis1 Hl x).
    + destruct H as [v ?].
      left. exists v.
      rewrite H.
      replace (subst_rgn k (Rgn2_Const true false e) (Rgn2_Const true true v)) with (Rgn2_Const true true v) by (simpl; reflexivity).
      apply subst_rho_rgn_const.
    + rewrite H.
      unfold subst_rgn.
      destruct (RMapP.eq_dec k x); subst; simpl.
      * left. exists e.
        apply subst_rho_rgn_const.
      * apply IHthis2.
Qed.

Lemma decompose_find_in_rho:
  forall x this1 this2 k e v t He Hl Hr,
    R.find (elt:=Region) x {| R.this := R.Raw.Node this1 k e this2 t; R.is_bst := He |} = Some v ->
    R.find (elt:=Region) x {| R.this := this1; R.is_bst := Hl |} = Some v \/
    R.find (elt:=Region) x {| R.this := this2; R.is_bst := Hr |} = Some v \/
    e = v.
Proof.
  intros.
  apply RMapP.find_mapsto_iff  in H.
  inversion H; subst.
  - right. right. reflexivity.
  - left. apply RMapP.find_mapsto_iff. auto.
  - right. left.  apply RMapP.find_mapsto_iff. auto.
Qed.

Lemma subst_rho_fvar_2:
  forall rho x v,
   find_R (Rgn2_FVar true false x) rho = Some v ->
   fold_subst_rgn rho (Rgn2_FVar true true x) = Rgn2_Const true true v.
Proof.
  intro rho.
  destruct rho.
  induction this; intros x v H.
  - unfold fold_subst_rgn, R.fold, R.Raw.fold; simpl.
    inversion H.
  - assert (Hl: R.Raw.bst this1) by (inversion is_bst; auto).
    assert (Hr: R.Raw.bst this2) by (inversion is_bst; auto).
    replace (fold_subst_rgn {| R.this := R.Raw.Node this1 k e this2 t; R.is_bst := is_bst |}
                            (Rgn2_FVar true true x))
    with
    (fold_subst_rgn {| R.this := this2; R.is_bst := Hr |}
                    (subst_rgn k (Rgn2_Const true false e)
                               (fold_subst_rgn {| R.this := this1; R.is_bst := Hl |} (Rgn2_FVar true true x)))
    ) by (unfold fold_subst_rgn, R.fold, R.Raw.fold in *; reflexivity).
    simpl in H.
    eapply decompose_find_in_rho in H; eauto.
    destruct H.
    + assert (H' : fold_subst_rgn {| R.this := this1; R.is_bst := Hl |}
                                 (Rgn2_FVar true true x) = Rgn2_Const true true v)
       by (apply IHthis1; simpl; assumption).
      rewrite H'. simpl. rewrite subst_rho_rgn_const. reflexivity.
    + destruct H.
      * assert (H'' : fold_subst_rgn {| R.this := this2; R.is_bst := Hr |}
                                 (Rgn2_FVar true true x) = Rgn2_Const true true v)
          by (apply IHthis2; simpl; assumption).
        admit.
      * subst.
Admitted.

Lemma NotNoneIsSome:
  forall {A} x,
    x <> None <-> exists a : A, x = Some a.
Proof.
  intuition.
  - destruct x.
    + exists a. reflexivity.
    + contradict H. reflexivity.
  - subst. destruct H. inversion H.
Qed.

Lemma TcRhoIncludedNoFreeVarsTyRef:
  forall rho rgns r0 t x,
    TcRho (rho, rgns) ->
    included (set_union (free_rgn_vars_in_rgn2 r0) (frv t)) rgns ->
    ~ free_rgn_vars_in_rgn2 (fold_subst_rgn rho r0) x.
Proof.
  intros rho rgns r0 t x HRho HInc H.
  generalize dependent r0.
  unfold rgn2_in_typ.
  dependent induction r0; intros.
  - rewrite subst_rho_rgn_const in H.
    simpl in H. contradiction.
  - destruct (AsciiVars.eq_dec x n) as [c | c].
    + inversion c; subst.
      inversion HRho; subst.
      contradict H.
      destruct (subst_rho_fvar_1 rho n) as [[v H0] | H0].
      * rewrite H0. simpl. intro. contradiction.
      * rewrite H0. simpl. intro.
        unfold set_elem, In in H1.
        destruct H1 with (r:=n).
        { apply H3 in HInc.
          - apply NotNoneIsSome in HInc.
            destruct HInc.
            apply subst_rho_fvar_2 in H4.
            rewrite H4 in H0.
            inversion H0.
          - apply Union_introl. simpl. auto. }
   + unfold AsciiVars.eq in c; subst.
     inversion HRho; subst.
     contradict H.
     destruct (subst_rho_fvar_1 rho n) as [[v H0] | H0].
     * rewrite H0. simpl. intro. contradiction.
     * rewrite H0. simpl. intro. inversion H. auto.
  - rewrite subst_rho_index in H.
    simpl in H. contradiction.
Qed.

Lemma TcRhoIncludedNoFreeVarsRgn_aux_fold:
  forall rho r x,
    free_rgn_vars_in_rgn2 (fold_subst_rgn rho r) x ->
    free_rgn_vars_in_rgn2 r x.
Proof.
  intros.
  unfold rgn2_in_typ in r; dependent induction r.
  - rewrite subst_rho_rgn_const in H. assumption.
  - assert ((exists v, fold_subst_rgn rho (Rgn2_FVar true true n) = Rgn2_Const true true v) \/
            fold_subst_rgn rho (Rgn2_FVar true true n) = Rgn2_FVar true true n)
      by (apply subst_rho_fvar_1).
    destruct H0.
    + destruct H0. rewrite H0 in H.
      unfold free_rgn_vars_in_rgn2 in H. inversion H.
    + rewrite H0 in H.
      assumption.
  - rewrite subst_rho_index in H. assumption.
Qed.

Lemma TcRhoIncludedNoFreeVarsSa_aux_fold:
  forall rho sa x,
    free_rgn_vars_in_sa2 (fold_subst_sa rho sa) x ->
    free_rgn_vars_in_sa2 sa x.
Proof.
  intros.
  induction sa; unfold free_rgn_vars_in_sa2, fold_subst_sa in *;
  eapply TcRhoIncludedNoFreeVarsRgn_aux_fold; eauto.
Qed.

Lemma TcRhoIncludedNoFreeVarsEps_aux_fold:
  forall rho e x,
    free_rgn_vars_in_eps2 (fold_subst_eps rho e) x ->
    free_rgn_vars_in_eps2 e x.
Proof.
  intros. unfold  free_rgn_vars_in_eps2, fold_subst_eps in *.
  destruct H as [sa [[sa' [H1 H2]] H3]].
  exists sa'. intuition.
  rewrite <- H2 in H3.
  eapply TcRhoIncludedNoFreeVarsSa_aux_fold; eauto.
Qed.

Lemma TcRhoIncludedNoFreeVarsSa:
  forall k rc r x,
    free_rgn_vars_in_rgn2 (subst_rgn k (Rgn2_Const true false rc) r) x ->
    free_rgn_vars_in_rgn2 r x.
Proof.
  intros.
  unfold rgn2_in_typ in r.
  dependent induction r;
  unfold free_rgn_vars_in_rgn2, subst_rgn in *; simpl.
  - inversion H.
  - destruct (RMapProp.F.eq_dec k n); subst; simpl in *.
    + inversion H.
    + assumption.
  - inversion H.
Qed.

Lemma TcRhoIncludedNoFreeVarsRgn:
  forall k rc sa x,
    free_rgn_vars_in_sa2 (subst_sa k (Rgn2_Const true false rc) sa) x ->
    free_rgn_vars_in_sa2 sa x.
Proof.
  intros.
  dependent induction sa;
  unfold free_rgn_vars_in_sa2, subst_sa in *; simpl;
  eapply TcRhoIncludedNoFreeVarsSa; eauto.
Qed.

Lemma TcRhoIncludedNoFreeVarsEps:
  forall k rc x e,
    (free_rgn_vars_in_eps2 (subst_eps k (Rgn2_Const _ _ rc) e)) x ->
    (free_rgn_vars_in_eps2 e) x.
Proof.
  intros.
  unfold free_rgn_vars_in_eps2 in *.
  destruct H as [sa H].
  unfold subst_eps in H.
  destruct H as [H1 H2].
  destruct H1 as [sa' H3].
  exists sa'; intuition.
  rewrite <- H0 in H2.
  eapply TcRhoIncludedNoFreeVarsRgn; eauto.
Qed.

Lemma TcRhoIncludedNoFreeVarsEps_included:
  forall k rc e,
    included
      (free_rgn_vars_in_eps2 (subst_eps k (Rgn2_Const _ _ rc) e))
      (free_rgn_vars_in_eps2 e).
Proof.
  intros k rc e.
  unfold included, Included, In.
  intro. intro.
  eapply TcRhoIncludedNoFreeVarsEps; eauto.
Qed.

Lemma TcRhoIncludedNoFreeVarsSa_aux:
  forall x rc sa,
    ~ free_rgn_vars_in_sa2 (subst_sa x (Rgn2_Const true false rc) sa) x.
Proof.
  intros.
  induction sa; unfold subst_sa in *;
  unfold rgn2_in_typ in r; dependent induction r; simpl;
  try (solve [ intro; contradict H |
               intro; unfold free_rgn_vars_in_rgn2 in H;
               destruct (RMapProp.F.eq_dec x n); subst;
               [inversion H | inversion H; symmetry in H0; contradiction] ]).
Qed.

Lemma TcRhoIncludedNoFreeVarsEps_aux:
  forall x e0 e,
  ~ free_rgn_vars_in_eps2 (subst_eps x (Rgn2_Const true false e0) e) x.
Proof.
  intros.
  unfold subst_in_eff.  intro.
  unfold free_rgn_vars_in_eps2, subst_eps in *.
  destruct H as [sa [H1 H2]].
  destruct H1 as [sa' [H3 H4]].
  rewrite <- H4 in H2.
  eapply TcRhoIncludedNoFreeVarsSa_aux; eauto.
Qed.

Module RProofs := R.Raw.Proofs.
Lemma FindIfLowerThan:
  forall x this1 this2 k e t is_bst H,
    R.find (elt:=Region) x
        {| R.this := R.Raw.Node this1 k e this2 t; R.is_bst := is_bst |} <> None ->
    R.Raw.lt_tree k this1 ->
    AsciiVars.lt x k ->
    R.find (elt:=Region) x {| R.this := this1; R.is_bst := H |} <> None.
Proof.
  intros x this1 this2 k e t is_bst H H1 H2 H3.
  assert (~ R.Raw.In k this1) by (apply RProofs.lt_tree_not_in in H2; auto).
  apply RProofs.in_find; auto.
  apply RProofs.find_in in H1.
  contradict H0.
  inversion H1; subst.
  - unfold AsciiVars.lt in H3; omega.
  - apply RProofs.lt_tree_not_in in H2.
    (*eapply RProofs.In_1 with (x:=k); eauto.*)
    (*  H2 : ~ R.Raw.In k this1
        H3 : AsciiVars.lt x k
        H4 : R.Raw.In x this1
        ============================
        R.Raw.In k this1 *)
    admit.
  - admit.
Admitted.

Lemma FindIfGreaterThan:
  forall x this1 this2 k e t is_bst H,
    R.find (elt:=Region) x
        {| R.this := R.Raw.Node this1 k e this2 t; R.is_bst := is_bst |} <> None ->
    R.Raw.gt_tree k this2 ->
    AsciiVars.lt k x ->
    R.find (elt:=Region) x {| R.this := this2; R.is_bst := H |} <> None.
Proof.
  intros x this1 this2 k e t is_bst H H1 H2 H3.
  assert (~ R.Raw.In k this2) by (apply RProofs.gt_tree_not_in in H2; auto).
  apply RProofs.in_find; auto.
  apply RProofs.find_in in H1.
  contradict H0.
  inversion H1; subst.
  - unfold AsciiVars.lt in H3; omega.
  - admit.
  - admit.
Admitted.

Lemma TcRhoIncludedNoFreeVarsEps_find:
  forall rho x,
    R.find x rho <> None ->
    forall e,
      ~ (free_rgn_vars_in_eps2 (fold_subst_eps rho e)) x.
Proof.
  intros rho. destruct rho. induction this; intros x H e'.
  - unfold fold_subst_eps.
    replace (fun sa : StaticAction2 =>
               exists sa' : StaticAction2,
                 e' sa' /\
                 fold_subst_sa {| R.this := R.Raw.Leaf nat; R.is_bst := is_bst |} sa' =
                 sa)
    with e' by (rewrite <- fold_eps_leaf with (is_bst := is_bst); reflexivity).
    intro. unfold R.find, R.Raw.find in H. simpl in H. contradict H. reflexivity.
  - inversion is_bst; subst.
    replace (fold_subst_eps
               {| R.this := R.Raw.Node this1 k e this2 t; R.is_bst := is_bst |} e')
    with (fold_subst_eps {| R.this := this2; R.is_bst := H6 |}
                         (subst_eps k (Rgn2_Const true false e)
                                    (fold_subst_eps {| R.this := this1; R.is_bst := H4 |} e')))
    by (rewrite <- fold_eps_node with (Hr:=H6) (Hl:=H4); reflexivity).
    intro.
    destruct (AsciiVars.compare x k); subst.
    + apply TcRhoIncludedNoFreeVarsEps_aux_fold in H0.
      apply TcRhoIncludedNoFreeVarsEps in H0.
      contradict H0.
      apply IHthis1.
      eapply FindIfLowerThan; eauto.
    + inversion e0; subst.
      apply TcRhoIncludedNoFreeVarsEps_aux_fold in H0.
      contradict H0.
      apply TcRhoIncludedNoFreeVarsEps_aux.
    + contradict H0.
      apply IHthis2.
      eapply FindIfGreaterThan; eauto.
Qed.

Lemma TcRhoIncludedNoFreeVarsEps_main:
  forall rho rgns e x,
    TcRho (rho, rgns) ->
    free_rgn_vars_in_eps2 e x ->
    included (free_rgn_vars_in_eps2 e) rgns ->
    ~ (free_rgn_vars_in_eps2 (fold_subst_eps rho e)) x.
Proof.
  intros.
  apply TcRhoIncludedNoFreeVarsEps_find.
  inversion H; subst. apply H3. apply H1.
  unfold In.
  assumption.
Qed.

Lemma TcRhoIncludedNoFreeVars:
  forall rho rgns t r,
    TcRho (rho, rgns) ->
    included (frv t) rgns ->
    r # subst_rho rho t.
Proof.
  intros.
  generalize dependent t.
  dependent induction t; intro HInc; simpl in HInc.
  - rewrite subst_rho_natural; simpl. intro. contradiction.
  - rewrite subst_rho_boolean; simpl. intro. contradiction.
  - rewrite subst_rho_effect; simpl. intro. contradiction.
  - rewrite subst_rho_unit; simpl. intro. contradiction.
  - rewrite subst_rho_pair; simpl.
    unfold not_set_elem, Complement. intro.
    destruct H0.
    + contradict H0. apply IHt1.
      unfold included, Included in *.
      intros. apply HInc.
      apply Ensembles.Union_introl.
      assumption.
    + contradict H0. apply IHt2.
      unfold included, Included in *.
      intros. apply HInc.
      apply Ensembles.Union_intror.
      assumption.
  - rewrite subst_rho_tyref; simpl.
    unfold not_set_elem, Complement. intro.
    destruct H0.
    + apply IHt.
      * unfold included, Included in *.
        intros. apply HInc.
        apply Ensembles.Union_intror.
        assumption.
      * contradict H0. unfold Ensembles.In.
        eapply TcRhoIncludedNoFreeVarsTyRef; eauto.
    + unfold included, Included, Ensembles.In in *.
      apply IHt.
      * intros. apply HInc. apply Ensembles.Union_intror. assumption.
      * assumption.
  - rewrite subst_rho_arrow; simpl.
    unfold not_set_elem, Complement. intro.
    destruct H0.
    + apply IHt1; auto.
      unfold included, Included in *.
      intros. apply HInc. apply Union_introl. assumption.
    + destruct H0.
      * { destruct H0.
          - eapply TcRhoIncludedNoFreeVarsEps_main  with (e:=e); eauto.
            + unfold In in H0. eapply TcRhoIncludedNoFreeVarsEps_aux_fold; eauto.
            + unfold included, Included, Ensembles.In in *.
              intro. intro.
              apply HInc.
              apply Ensembles.Union_intror. apply Ensembles.Union_introl.
              apply Ensembles.Union_introl. assumption.
          - eapply TcRhoIncludedNoFreeVarsEps_main with (e:=e0); eauto.
            + unfold In in H0. eapply TcRhoIncludedNoFreeVarsEps_aux_fold; eauto.
            + unfold included, Included, Ensembles.In in *.
              intro. intro. apply HInc.
              apply Ensembles.Union_intror. apply Ensembles.Union_introl.
              apply Ensembles.Union_intror. assumption. }
      * { repeat destruct H0.
          - apply IHt2; auto.
            unfold included, Included in *.
            intros. apply HInc.
            apply Union_intror. apply Union_intror. apply Union_introl. assumption.
          - apply IHt3; auto.
            unfold included, Included in *.
            intros. apply HInc.
            apply Union_intror. apply Union_intror. apply Union_intror. assumption. }
  - rewrite subst_rho_forallrgn; simpl.
    unfold not_set_elem, Complement. intro.
    destruct H0.
    + eapply TcRhoIncludedNoFreeVarsEps_main with (e:=e); eauto.
      * eapply TcRhoIncludedNoFreeVarsEps_aux_fold; eauto.
      * unfold included, Included, In in *. intro. intro.
        apply HInc.
        apply Union_introl. assumption.
    + apply IHt; auto.
      unfold included, Included in *.
      intros. apply HInc.
      apply Union_intror. assumption.
Qed.

author: esmifro

repo: SurfaceEffects

save_path: github-repos/coq/esmifro-SurfaceEffects


text:
From fae_gtlc_mu.stlc_mu Require Export contexts typing.
From fae_gtlc_mu.cast_calculus Require Export contexts typing.
From fae_gtlc_mu.embedding Require Export expressions types well_typedness.
From fae_gtlc_mu.backtranslation Require Export expressions well_typedness.

Definition Halts_stat := stlc_mu.lang.Halts.

Section gradual_static.
  From fae_gtlc_mu.refinements.gradual_static Require Export adequacy.
  From fae_gtlc_mu.refinements.gradual_static Require Export rel_ref_specs.

  Lemma gradual_static (Γ : list stlc_mu.types.type) (e : cast_calculus.lang.expr) (τ : stlc_mu.types.type) (pτ : stlc_mu.types.Closed τ) (de : (map embed_type Γ) ⊢ₜ e : (embed_type τ)):
    ∀ (Cₛ : stlc_mu.contexts.ctx), stlc_mu.contexts.typed_ctx Cₛ Γ τ [] stlc_mu.types.TUnit →
       Halts_grad (fill_ctx (embed_ctx Cₛ) e) →
       Halts_stat (stlc_mu.contexts.fill_ctx Cₛ (backtranslate_expr e)).
  Proof.
    intros Cₛ dCₛ Hs.
    apply (@adequacy actualΣ _ _ (fill_ctx (embed_ctx Cₛ) e) _ (embed_type stlc_mu.types.TUnit)); auto. intros.
    assert ([] = map embed_type []) as ->. done.
    apply (embed_ctx_relates Γ _ _ τ); auto.
    apply (back_relates (map embed_type Γ) e (embed_type τ)); auto.
  Qed.

End gradual_static.

From fae_gtlc_mu Require Export fae. (* for the static_ctx_refines_gradual_easy lemma and the retract lemma *)

Definition stuck_diverge_grad : cast_calculus.lang.expr → Prop :=
  fun e => ¬ cast_calculus.lang.Halts e.

Definition stuck_diverge_stat : stlc_mu.lang.expr → Prop :=
  fun e => ¬ stlc_mu.lang.Halts e.

Definition stat_P C Γ τ : Prop :=
    (stlc_mu.types.Closed τ) ∧ (stlc_mu.contexts.typed_ctx C Γ τ [] stlc_mu.types.TUnit)
  ∧ (∀ e, Γ ⊢ₛ e : τ → stuck_diverge_stat (stlc_mu.contexts.fill_ctx C e)).

Definition grad_P C Γ τ : Prop :=
    (cast_calculus.types.Closed τ) ∧ (cast_calculus.contexts.typed_ctx C Γ τ [] cast_calculus.types.TUnit)
  ∧ (∀ e, Γ ⊢ₜ e : τ → stuck_diverge_grad (cast_calculus.contexts.fill_ctx C e)).

(** stat_P and grad_P are the properties on contexts that we want to preserve and reflect *upon embedding* *)

Theorem preservation C Γ τ (Hs : stat_P C Γ τ) : grad_P (embed_ctx C) (map embed_type Γ) (embed_type τ).
Proof.
  destruct Hs as [pτ [pC Hs] ].
  split; try split. by apply embd_closed. cut (typed_ctx (embed_ctx C) (map embed_type Γ) [|τ|] (map embed_type []) (embed_type stlc_mu.types.TUnit)). auto.
  apply embedding.well_typedness.well_typedness_ctx; auto.
  intros eₜ deₜ abs. apply (Hs (backtranslate_expr eₜ)).
  cut (map backtranslate_type (map embed_type Γ) ⊢ₛ backtranslate_expr eₜ : backtranslate_type (embed_type τ)).
  rewrite map_map (map_ext _ id). by rewrite map_id retract. intro. by rewrite retract.
  by apply backtranslation.well_typedness.well_typedness_expr.
  apply (gradual_static Γ _ τ); auto.
Qed.

Theorem reflection C Γ τ (pτ : stlc_mu.types.Closed τ) (dC : stlc_mu.contexts.typed_ctx C Γ τ [] stlc_mu.types.TUnit) :
  (grad_P (embed_ctx C) (map embed_type Γ) (embed_type τ)) → stat_P C Γ τ.
Proof.
  intro Hg. destruct Hg as [peτ [peC Hg] ].
  split; try split; auto.
  intros e de abs. apply (Hg (embed_expr e)). by apply embedding.well_typedness.well_typedness_expr.
  by eapply static_ctx_refines_gradual_easy.
Qed.

author: scaup

repo: fae-gtlc-mu

save_path: github-repos/coq/scaup-fae-gtlc-mu