text:
Require Import Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes Undecidability.Shared.Libs.PSL.Vectors.Vectors.
Require Import Vector List.

Require Import Undecidability.TM.Util.TM_facts.

From Undecidability Require Import ProgrammingTools WriteValue Copy ListTM  JumpTargetTM WriteValue.
From Undecidability.TM.L Require Import Alphabets LookupTM.
From Undecidability.L.AbstractMachines.FlatPro Require Import LM_heap_def LM_heap_correct UnfoldClos.
From Undecidability.TM Require Import CaseList CasePair CaseCom CaseNat NatSub.

From Undecidability Require Import L.L TM.TM Hoare.

From Undecidability.L.Prelim Require Import LoopSum.

Require Import Ring Arith.

Import VectorNotations.
Import ListNotations.
Import Coq.Init.Datatypes List.

Open Scope string_scope.
Require Import String.

Set Default Proof Using "Type".

From Undecidability Require Cons_constant.

Module Private_UnfoldClos.
Section Fix.

  Variable Σ : finType.

  Variable retr_stack : Retract (sigList (sigPair sigHClos sigNat)) Σ.
  Variable retr_heap : Retract sigHeap Σ.

  Definition retr_clos : Retract sigHClos Σ := ComposeRetract retr_stack _.

  Definition retr_pro : Retract sigPro Σ := ComposeRetract retr_clos _.
  Definition retr_com : Retract sigCom Σ := ComposeRetract retr_pro _.

  Definition retr_nat_clos_ad' : Retract sigNat sigHClos := Retract_sigPair_X _ _.
  Definition retr_nat_clos_ad : Retract sigNat Σ := ComposeRetract retr_clos retr_nat_clos_ad'.

  Definition retr_nat_clos_var' : Retract sigNat sigHClos := Retract_sigPair_Y _ _.
  Definition retr_nat_clos_var : Retract sigNat Σ := ComposeRetract retr_clos retr_nat_clos_var'.

  Definition retr_stackEl : Retract (sigPair sigHClos sigNat) Σ :=
    (ComposeRetract retr_stack _).

  Definition retr_nat_stack : Retract sigNat Σ :=
    ComposeRetract retr_stackEl
            (Retract_sigPair_Y _ _) .

  (* Instance of the [Lookup] and [JumpTarget] machine *)
  Local Definition Lookup := Lookup retr_clos retr_heap.

  Local Notation i_H := Fin0 (only parsing).
  Local Notation i_a := Fin1 (only parsing).
  Local Notation i_P := Fin2 (only parsing).
  Local Notation i_k := Fin3 (only parsing).
  Local Notation i_stack' := Fin4 (only parsing).
  Local Notation i_res := Fin5 (only parsing).
  Local Notation i_aux1 := Fin6 (only parsing).
  Local Notation i_aux2 := Fin7 (only parsing).
  Local Notation i_aux3 := Fin8 (only parsing).
  Local Notation i_aux4 := Fin9 (only parsing).

    (* Print unfoldTailRecStep. *)
    (*
      Definition unfoldTailRecStep '(stack,res) : (list (HClos*nat) * Pro) + option Pro :=
  match stack with
    | ((a,P),k)::stack =>
      match P with
        c::P =>
          match c with
            varT n =>
              if ( k <=? n)
              then
                  match lookup H a (n-k) with
                  | Some (b,Q) =>
                    inl (((b,Q),1)::(a,retT::P,S k)::stack,lamT::res)
                  | None => inr None
                  end
              else
                inl ((a,P,k)::stack,varT n::res)
          | appT => inl ((a,P,k)::stack,appT::res)
          | lamT => inl ((a,P,S k)::stack,lamT::res)
          | retT => inl ((a,P,pred k)::stack,retT::res)
          end
        | [] => inl (stack,res)
      end
    | [] => inr (Some res)
  end.
  *)

  Definition M__step : pTM (Σ) ^+ (option unit) 10 :=
    If
      (CaseList _ ⇑ retr_pro @ [| i_P;i_aux1|])
      (Switch (CaseCom ⇑ retr_com @ [|i_aux1|])
        (fun i : option ACom=> match i with
          | Some c =>
            Cons_constant.M (ACom2Com c)⇑ retr_pro @ [| i_res|];;
            Return
            match c return match c with _ => _ end with
            | retAT => (CaseNat ⇑ retr_nat_clos_var @ [|i_k|];;Return Nop tt)
            | lamAT => Constr_S  ⇑ retr_nat_clos_var @ [|i_k|]
            | appAT => Nop
            end
            None
          | None (*var*) =>
            CopyValue _  @ [| i_k;i_aux2|];;
            CopyValue _  @ [| i_aux1;i_aux3|];;
            If (Subtract ⇑ retr_nat_clos_var @ [|i_aux3;i_aux2|])
               (Reset _ @ [|i_aux1|];;
                CopyValue _  @ [| i_a;i_aux4|];;
                If (Lookup @ [|i_H;i_aux4;i_aux3;i_aux1;i_aux2|])
                  (Cons_constant.M lamT⇑ retr_pro @ [| i_res|];;
                   Cons_constant.M retT⇑ retr_pro @ [| i_P|];;
                   Constr_S  ⇑ retr_nat_clos_var @ [|i_k|];;
                   Constr_pair _ _ ⇑ retr_clos @ [|i_a;i_P|];;
                   Reset _ @ [|i_a|];;
                   Translate retr_nat_clos_var retr_nat_stack @[|i_k|];;
                   Constr_pair _ _ ⇑ retr_stackEl @ [|i_P;i_k|];;
                   MoveValue _ @ [|i_aux1;i_P|];;
                   Constr_cons _ ⇑ retr_stack @ [| i_stack';i_k|];;
                   Reset _ @ [|i_k|];;
                   CasePair _ _ ⇑ retr_clos @ [|i_P;i_a|];;
                   Return (WriteValue ( 1) ⇑ retr_nat_clos_var @ [|i_k|]) None
                  )
                  (Return Diverge (Some tt))
               )
               (Return
                 (Constr_varT ⇑ retr_com @ [|i_aux1|];;
                  Constr_cons _ ⇑ retr_pro @ [| i_res;i_aux1|];;
                  Reset _  @ [|i_aux1|];;
                  Reset _ @ [|i_aux3|])
                 None)
        end)
      )
      ( Reset _ @ [|i_P|];;
        Reset _ @ [|i_a|];;
        Reset _ @ [|i_k|];;
        If
          (CaseList _ ⇑ retr_stack @ [| i_stack';i_k|])
          (CasePair _ _ ⇑ retr_stackEl @ [|i_k;i_P|];;
           CasePair _ _ ⇑ retr_clos @ [|i_P;i_a|];;
           Translate retr_nat_stack retr_nat_clos_var @[|i_k|];;
           Return Nop None
          )
          (Reset _ @ [|i_stack'|];;Return Nop (Some tt))
      ).

  Local Arguments "+"%nat : simpl never.
  Local Arguments "*"%nat : simpl never.

  Local Arguments UpToC.f__UpToC {_ _} _ _.
  Open Scope nat_scope.

  (* This function is copied from the end of the proof of SpecT__step' and not written by hand*)
  Definition steps_step H (stack : list (HAdd * list Tok * nat)) :=
    match stack with
      (a,P,k)::stack' =>
    1 + CaseList_steps P +
      (if match P with
          | [] => false
          | _ :: _ => true
          end
      then
        match P with
        | [] => 0
        | t :: P0 =>
            match t with
            | varT n =>
                1 + CaseCom_steps +
                (1 + CopyValue_steps k +
                (1 + CopyValue_steps n +
                  (1 + UpToC.f__UpToC (projT1 Subtract_SpecT) k +
                  (if k <=? n
                    then
                    1 + Reset_steps n +
                    (1 + CopyValue_steps a +
                      match lookup H a (n - k) with
                      | Some h =>
                          let (_, _) := h in
                          Lookup_steps H a (n - k) + Cons_constant.time lamT +
                          Cons_constant.time retT + Constr_S_steps +
                          Constr_pair_steps a + Reset_steps a +
                          Translate_steps (1 + k) +
                          Constr_pair_steps (a, retT :: P0) +
                          MoveValue_steps h (a, retT :: P0) +
                          Constr_cons_steps (a, retT :: P0, 1 + k) +
                          Reset_steps (a, retT :: P0, 1 + k) +
                          CasePair_steps (fst h) + WriteValue_steps 2 +
                          Pos.to_nat 11 + 1
                      | None => 0
                      end)
                    else
                    Constr_varT_steps + Constr_cons_steps t + Reset_steps t +
                    Reset_steps (n - k) + Pos.to_nat 3))))
            | _ => 1 + CaseCom_steps + 16
            end
        end
      else
        1 + Reset_steps P +
        (1 + Reset_steps a +
        (1 + Reset_steps k +
          (1 + CaseList_steps stack' +
          (if match stack' with
              | [] => false
              | _ :: _ => true
              end
            then
            match stack' with
            | [] => 0
            | p :: _ =>
                let (p0, _) := p in
                let (_, _) := p0 in
                1 + CasePair_steps (fst p) +
                (1 + CasePair_steps (fst p0) + (1 + Translate_steps (snd p) + 0))
            end
            else
            match stack' with
            | [] => 1 + Reset_steps stack' + 0
            | _ :: _ => 0
            end)))))
  | _ => 0
  end.

  Arguments steps_step : simpl never.

  Lemma SpecT__step (H:Heap) a P k (stack' : list (HAdd * list Tok * nat)) res nextState n' finalRes:
      TripleT
      ≃≃([unfoldTailRecStep H (((a,P),k)::stack',res)%list = inl nextState;
          loopSum n' (unfoldTailRecStep H) (((a,P),k)::stack',res) = Some (Some finalRes)],
      [|Contains retr_heap H;Contains retr_nat_clos_ad a;Contains retr_pro P;Contains retr_nat_clos_var k; Contains retr_stack stack';
              Contains retr_pro res;Void;Void;Void;Void|])
      (steps_step H (((a,P),k)::stack') ) M__step
      (fun r => ≃≃([
      loopSum (pred n') (unfoldTailRecStep H) nextState = Some (Some finalRes);
      match r with Some tt => nextState = ([],finalRes) | _ => fst nextState <> [] end;n' <> 0]
          ,[|Contains _ H|]
          ++let (stack2,res2) := nextState in
            match stack2 with
            | []%list => Vector.const Void 4
            | ((a2,P2),k2)::stack2' => [|Contains retr_nat_clos_ad a2;Contains retr_pro P2;Contains retr_nat_clos_var k2;Contains retr_stack stack2'|]
            end%list
                ++[|Contains retr_pro res2;Void;Void;Void;Void|])).
  Proof.
    hintros HnS Hloop.
    eapply ConsequenceT with (Q2:=fun y => _). 2,3:reflexivity.
    unfold M__step.
    hstep.
    { cbn;hsteps_cbn. cbn. tspec_ext. }
    2:{
      destruct P;cbn;hintros [=]. cbn.
      hstep. now hsteps_cbn. 2:reflexivity.
      cbn. hintros _. hstep. now hsteps_cbn. 2:reflexivity.
      cbn. hintros _. hstep. now hsteps_cbn. 2:reflexivity.
      cbn. hintros _. hstep. {hsteps_cbn;cbn. tspec_ext. }
      all:cbn.
      - refine (_ : TripleT _ (match stack' with ((_,_),_)::_ => _ | _ => 0 end) _ _).
        destruct stack' as [ |[[]]]; hintros [=].
        injection HnS as [= <-].
        destruct n'. now inv Hloop. cbn in Hloop.
        remember (unfoldTailRecStep H ((h, l, n) :: stack', res)) as st.
        cbn. hsteps_cbn. 1-3:try now cbn;tspec_ext. all:reflexivity. (*
        destruct n'. now inv Hloop.
        cbn - [unfoldTailRecStep] in Hloop|-*. rewrite <- Heqst in Hloop|-*.
        destruct st. 2:{inv Hloop. tspec_ext. }
        tspec_ext. all: easy. *)
      - refine (_ : TripleT _ (match stack' with []=> _ | _ => 0 end) _ _).
        destruct stack';hintros [=].
        injection HnS as [=<-].
        hsteps_cbn.
        { destruct n' as [|[]]. 1,2:now discriminate Hloop. injection Hloop as ->. now tspec_ext. }
        reflexivity.
      -intros ? ->. reflexivity.
    }
    2:{cbn [fst implList]. intros ? ->. reflexivity. }
    cbn. refine (_ : TripleT _ (match P with [] => _ | t::P => match t with appT => _ | _ => _ end end) _ _).
    destruct P;hintros [=]. cbn in HnS.
    eapply Switch_SpecTReg.
    {cbn. hsteps_cbn. cbn. tspec_ext. }
    {
      destruct n'. 1:easy. cbn in Hloop. rewrite HnS in Hloop.
      remember (unfoldTailRecStep H nextState) as ns'.
      cbn. hintros [ y| ] Hy.
      - subst t. cbn.
        hstep. {hsteps_cbn. cbn. tspec_ext. }
        cbn. intros _.
        hstep.
        +refine (_:TripleT _ (match y with retAT => _ | _ => _ end) _ (fun x => ≃≃([],match y with retAT => _ | _ => _ end))).
         destruct y;cbn.
         all:hsteps_cbn;cbn.
         --now tspec_ext.
         --hintros y' Hy'. hsteps_cbn;cbn. tspec_ext.
         --reflexivity.
         --cbn. tspec_ext.
         --cbn. eapply ConsequenceT. apply Nop_SpecT. all:try reflexivity. cbn;intros. tspec_ext.
        +cbn. destruct y;cbn in HnS|-*. all:injection HnS as [= <-];cbn.
         all:intro;tspec_ext;easy.
        +unfold Constr_S_steps,Cons_constant.time.
         destruct y;cbn. refine (_ : _ <= (fun x => match x with Some _ => 16 | _ => _ end) _);[|shelve].
         all:unfold CaseNat_steps;lia.
      - destruct Hy as (x&Ht).
        refine (_ : TripleT _ (match t with varT x => _ | _ => 0 end) _ _).
        subst t.
        hstep. now hsteps_cbn. 2:reflexivity.
        cbn. intro. hstep. now hsteps_cbn.
        cbn. intro. hstep.
        +cbn. hsteps_cbn. cbn. tspec_ext.
        +hintros Hlt. rewrite <- Hlt in HnS. cbn.
          hstep. now hsteps_cbn. 2:reflexivity.
          cbn;intros _. hstep. now hsteps_cbn. 2:reflexivity.
          cbn;intros _.
          refine (_ : TripleT _ match lookup H a (x-k) with Some (_,_) => _ | _ => 0 end _ _).
          hstep. 1:{ hsteps_cbn;cbn. refine (TripleT_RemoveSpace _ (Q:= fun _ => _) (Q':= fun _ => _));intros.
          eapply ConsequenceT. eapply Lookup_SpecT_space. now tspec_ext. cbn. intros. reflexivity. reflexivity. }
          destruct lookup as [[]|]eqn:Hlook;hintros [=].
          *injection HnS as [= <-]. cbn. hsteps_cbn;cbn.
           1-4:try tspec_ext.
           { eapply ConsequenceT. notypeclasses refine (Translate_SpecT _ _ _ _ ).
            3:tspec_ext. cbn;intro. all:reflexivity.
            }
            1-5:cbn;try solve [tspec_ext].
            now tspec_ext. 1-10:reflexivity.
            refine (_ : _ <= match lookup H a (x-k) with Some (_,_) => _ | _ => 0 end).
            rewrite Hlook. ring_simplify. reflexivity.
          * destruct lookup eqn:Hlook;hintros [=]. now exfalso.
          * cbn. destruct lookup as [[]|]. 2:exfalso;easy.
            intros ? ->. ring_simplify; reflexivity.
        + cbn. hintros Hlt. rewrite <- Hlt in HnS.
          injection HnS as [= <-]. cbn.
          hsteps_cbn;cbn. 1-2:now tspec_ext. 1-2:reflexivity. ring_simplify;reflexivity. now tspec_ext.
        +cbn. intros ? ->. reflexivity.
        +reflexivity.
     }
     cbn. intros [c|] Hy.
     2:{destruct Hy as (?&->). reflexivity. }
     rewrite Hy. destruct c;cbn;reflexivity.
     (* copy this to define steps_step, replacing holes with 0*)
     unfold steps_step. reflexivity. Unshelve. all:exact 0.
  Qed.

  Definition M__loop := While M__step.

  Local Arguments unfoldTailRecStep : simpl never.

  (*TODO: remove, already copied *)
  Lemma tspec_revertPure (sig: finType) (n : nat) (P0:Prop) P (Ps : SpecV sig n) Q:
  P0
  -> Entails (tspec (P0::P,Ps)) Q
  -> Entails (tspec (P,Ps)) Q.
  Proof.
    setoid_rewrite Entails_iff. unfold tspec;cbn. easy.
  Qed.

  (* This function is derived from the end of the proof of SpecT__step' and not written by hand*)
  Fixpoint steps_loop H n x :=
    match n with
      0 => 0
    | S n => 1 + steps_step H (fst x) +
      match unfoldTailRecStep H x with
        inl y=> steps_loop H n y
      | inr y=> 0
      end
    end.

  Set Keyed Unification.

  Lemma SpecT__loop (H:Heap) a P k (stack' : list (HAdd * list Tok * nat)) res n' finalRes:
    TripleT
      ≃≃([loopSum n' (unfoldTailRecStep H) (((a,P),k)::stack',res) = Some (Some finalRes)]
          ,[|Contains retr_heap H;Contains retr_nat_clos_ad a;Contains retr_pro P;Contains retr_nat_clos_var k; Contains retr_stack stack';
              Contains retr_pro res;Void;Void;Void;Void|])
      (steps_loop H n' ((a,P,k)::stack',res)) M__loop
      (fun r => ≃≃([]
          ,[|Contains _ H;Void;Void;Void;Void;Contains retr_pro finalRes;Void;Void;Void;Void|])).
  Proof.
    refine (While_SpecTReg _ _ (a,P,k,stack',res,n')
      (PRE := fun '(a,P,k,stack',res,n') => (_,_)) (POST := fun '(a,P,k,stack',res,n') y => (_,_))
      (INV := fun '(a,P,k,stack',res,n') y  => _ )
    (f__step := fun '(a,P,k,stack',res,n') => _)
    (f__loop := fun  '(a,P,k,stack',res,n') => _ ));
    clear a P k stack' res n';intros [[[[[a P] k]stack']res]n'].
    { hsteps_cbn.
      - hintros Hloop.
        eapply (ConsequenceT
            (Q1 := fun y =>  _)
            (Q2:= fun y => _)).
        now eapply (SpecT__step H a P k stack' res match unfoldTailRecStep H ((a, P, k) :: stack', res) with
            | inl x' => _ | _ => ([],[]) end _ _ ).
        3:reflexivity.
        { destruct unfoldTailRecStep eqn:H'. { tspec_ext. reflexivity. eassumption. }
          exfalso.
          destruct n'; cbn. now inv Hloop. cbn in Hloop. rewrite H' in Hloop.
          exfalso. unfold unfoldTailRecStep in H'. repeat destruct _ in H'. all:congruence. }
        { intros ?. reflexivity. }
    }
    cbn. split.
    + intros Hloop [] Hloop' Hloop'' Hn'. split.
     {
       destruct unfoldTailRecStep as [res'|]eqn:?.
       *subst res'. reflexivity.
       *injection Hloop'' as [= <-]. reflexivity.
     }
     destruct n'. now contradiction Hn'. cbn. nia.
    +intros Hloop' Hnil Hn'.
     destruct (unfoldTailRecStep H ((a, P, k) :: stack', res)) as [[[| [[a' P'] k'] stack''] res'']|] eqn:H' in Hloop',Hnil.
     {exfalso;clear - Hnil;easy. }
     clear Hnil.
     eexists (a',P',k',stack'',res'',(pred n')). split.
      -rewrite H'.
      rewrite Hloop'.  tspec_ext.
      - split. 2:easy. destruct n';cbn. exfalso;easy. rewrite H' at 1. reflexivity.
      -easy.
  Qed.

  Definition M :=
    WriteValue ( []) ⇑ retr_stack @ [|i_stack'|];;
    WriteValue ( []) ⇑ retr_pro @ [|i_res|];;
    M__loop.

  Definition steps H a k s s' := 2 * WriteValue_steps 1 +
        steps_loop H (L_facts.size s' * 3 + 2) ([(a, compile s, k)], []) + 2.

  Lemma SpecT (H:Heap) a k s s':
    unfolds H a k s s' ->
      TripleT
        ≃≃([]
            ,[|Contains retr_heap H;Contains retr_nat_clos_ad a;Contains retr_pro (compile s);Contains retr_nat_clos_var k; Void;
                Void;Void;Void;Void;Void|])
        (steps H a k s s') M
        (fun r => ≃≃([]
            ,[|Contains _ H;Void;Void;Void;Void;Contains retr_pro (rev (compile s'));Void;Void;Void;Void|])).
  Proof.
    unfold M. intros H'.
    eapply unfoldTailRecStep_complete in H'. 2:reflexivity.
    eapply ConsequenceT_pre. 2:reflexivity.
    hsteps_cbn;cbn. 1,2,4,5:reflexivity.
    eapply ConsequenceT_pre. 3:reflexivity.
    -eapply SpecT__loop.
    - rewrite H'. tspec_ext.
    -unfold steps. nia.
  Qed.

End Fix.
End Private_UnfoldClos.

Module UnfoldClos.
Section Fix.

  Variable Σ : finType.

  Variable retr_stack : Retract (sigList (sigPair sigHClos sigNat)) Σ.
  Variable retr_heap : Retract sigHeap Σ.

  Variable retr_clos : Retract sigHClos Σ.
  Definition retr_pro : Retract sigPro Σ := ComposeRetract retr_clos _.
  Definition retr_clos_stack : Retract sigHClos Σ := ComposeRetract retr_stack _.

  Definition retr_stackEl : Retract (sigPair sigHClos sigNat) Σ :=
    (ComposeRetract retr_stack _).
  Definition retr_nat_stack : Retract sigNat Σ :=
    ComposeRetract retr_stackEl
            (Retract_sigPair_Y _ _) .

  Local Notation n := 10 (only parsing).

  Local Notation i_io := Fin0 (only parsing).
  Local Notation i_H := Fin1 (only parsing).

  Definition M : pTM (Σ) ^+ unit n:=
    Translate retr_clos retr_clos_stack @[|i_io|];;
    CasePair _ _ ⇑ retr_clos_stack @ [|i_io;Fin2|];;
    WriteValue ( 1) ⇑ Private_UnfoldClos.retr_nat_clos_var retr_stack @ [|Fin3|];;
    Private_UnfoldClos.M retr_stack retr_heap @ [|i_H;Fin2;i_io;Fin3;Fin4;Fin5;Fin6;Fin7;Fin8;Fin9|];;
    Translate (Private_UnfoldClos.retr_pro retr_stack) retr_pro @ [|Fin5|];;
    WriteValue ( [retT]) ⇑ retr_pro @ [|i_io|];;
    Rev_Append _ ⇑ retr_pro @ [| Fin5;i_io;Fin6 |];;
    Cons_constant.M lamT ⇑ retr_pro @ [| i_io|].

  Definition steps H '(a',P) t' :=
    match t' with lam t' =>
    match decompile 0 P [] with
      inl [s'] =>
      1 + Translate_steps (a', compile s') +
      (1 + CasePair_steps (fst (a', compile s')) +
       (1 + WriteValue_steps (size 1) +
        (1 + Private_UnfoldClos.steps H a' 1 s' t' +
         (1 + Translate_steps (rev (compile t')) +
          (1 + WriteValue_steps (size [retT]) +
           (1 + Rev_Append_steps Encode_Com (rev (compile t')) +
            Cons_constant.time lamT))))))
      | _ => 0
    end
    | _ => 0 end.

  Lemma SpecT (H:Heap) g s:
      reprC H g s ->
      TripleT
        ≃≃([]
            ,[|Contains retr_clos g;Contains retr_heap H;Void;Void;Void;Void;Void;Void;Void;Void|])
        (steps H g s) M
        (fun r => ≃≃([]
          ,[|Contains retr_pro (compile s);Contains retr_heap H;Void;Void;Void;Void;Void;Void;Void;Void|])).
  Proof.
    unfold steps.
    intros (s'&t'&a'&Hg&Hs&Hunf)%reprC_elim_deep.
    remember (compile s) as P.
    subst g s. rewrite decompile_correct.
    unfold M.
    eapply ConsequenceT. 2:reflexivity.
    do 3 hstep_seq;[].
    hstep_seq;[|].
    {
      hsteps_cbn;cbn. eapply ConsequenceT_pre.
      now refine (Private_UnfoldClos.SpecT _ _ Hunf).
      now tspec_ext.
      reflexivity.
    }
    cbn.
    do 3 (hstep_seq;[]).
    hsteps_cbn. now tspec_ext. {intro;cbn. tspec_ext. f_equal. rewrite rev_involutive. now subst. }
    reflexivity.
  Qed.

(*
  Theorem Realise :
  Realise M (fun t '(r, t') =>
                      forall g (H : Heap) s,
                          reprC H g s
                          -> t[@i_io] ≃(retr_clos) g
                          -> t[@i_H] ≃ H
                          -> (forall i : Fin.t 8, isVoid t[@ Fin.R 2 i])
                          -> t'[@i_io] ≃(retr_pro) compile s
                          /\ t[@i_H] ≃ H
                          /\ (forall i : Fin.t 8, isVoid t'[@ Fin.R 2 i])).
*)

End Fix.
End UnfoldClos.

repo: coq-synthetic-incompleteness


text:
(** * General Facts about the Sitpn Structure. *)

Require Import CoqLib.
Require Import GlobalFacts.
Require Import sitpn.Sitpn.

Set Implicit Arguments.

(** For a given [sitpn], defines the equivalence relation [Peq]
    between two places as the equality between the first element
    of the [sig] type [P sitpn].  *)

Definition Peq sitpn (p p' : P sitpn) : Prop := P1SigEq p p'.

(** For a given [sitpn], defines the equivalence relation [Pkeq]
    between two pairs where places are the first elements of the
    pairs.  *)

Definition Pkeq sitpn {A : Type} (p p' : P sitpn * A) : Prop :=
  Peq (fst p) (fst p') /\ snd p = snd p'.

Arguments Peq {sitpn}.
Arguments Pkeq {sitpn A}.

(** The equivalence relation [Peq] is decidable. *)

Definition Peqdec sitpn (x y : P sitpn) : {Peq x y} + {~Peq x y} :=
  P1SigEqdec Nat.eq_dec x y.
Arguments Peqdec {sitpn}.

(* The [SetoidList.InA] predicate is decidable with [Peq] as the
   equality relation. *)

Definition InA_Peq_dec sitpn (p : P sitpn) (lofP : list (P sitpn)) :
  {SetoidList.InA Peq p lofP} + {~SetoidList.InA Peq p lofP} :=
  InA_P1SigEq_dec (fun n => In n sitpn.(places)) Nat.eq_dec p lofP.

(*  *)

Definition Equivalence_Peq sitpn := Equivalence_P1SigEq (In_P sitpn).

#[export] Hint Unfold Peq Pkeq Peqdec : core.

(** For a given [sitpn], defines the equivalence relation [Teq]
    between two transitions as the equality between the first element
    of the [sig] type [T sitpn].  *)

Definition Teq sitpn (t t' : T sitpn) : Prop := P1SigEq t t'.

(* SetoidList InA predicate is decidable if eq = Teq *)

Definition Teq' sitpn (Q : T sitpn -> Prop) (t t' : Tsubset Q) : Prop :=
  Teq (proj1_sig t) (proj1_sig t').

(** For a given [sitpn], defines the equivalence relation [Tkeq]
    between two pairs where transitions are the first elements of the
    pairs.  *)

Definition Tkeq sitpn {A : Type} (p p' : T sitpn * A) : Prop :=
  Teq (fst p) (fst p') /\ snd p = snd p'.

Arguments Teq {sitpn}.
Arguments Tkeq {sitpn A}.

(** The equivalence relation [Teq] is decidable. *)

Definition Teqdec sitpn (x y : T sitpn) : {Teq x y} + {~Teq x y} :=
  P1SigEqdec Nat.eq_dec x y.
Arguments Teqdec {sitpn}.

(** The equivalence relation [Teq'] is also decidable. *)

Definition Teq'_dec sitpn {Q : T sitpn -> Prop}
           (x y : Tsubset Q) : {Teq' x y} + {~Teq' x y} :=
  Teqdec (proj1_sig x) (proj1_sig y).
Arguments Teq'_dec {sitpn Q}.

(* The [SetoidList.InA] predicate is decidable with [Teq] as the
   equality relation. *)

Definition InA_Teq_dec sitpn (t : T sitpn) (lofT : list (T sitpn)) :
  {SetoidList.InA (@Teq sitpn) t lofT} + {~SetoidList.InA (@Teq sitpn) t lofT} :=
  InA_P1SigEq_dec (fun n => In n sitpn.(transitions)) Nat.eq_dec t lofT.

#[export] Hint Unfold Teq Tkeq Teqdec : core.

(** For a given [sitpn], defines the equivalence relation [Aeq]
    between two actions as the equality between the first element
    of the [sig] type [A sitpn].  *)

Definition Aeq sitpn (a a' : A sitpn) : Prop := P1SigEq a a'.
Arguments Aeq {sitpn}.

(** For a given [sitpn], defines the equivalence relation [Akeq]
    between two pairs where actions are the first elements of the
    pairs.  *)

Definition Akeq sitpn {B : Type} (p p' : A sitpn * B) : Prop := Aeq (fst p) (fst p') /\ snd p = snd p'.

Arguments Akeq {sitpn B}.

(** The equivalence relation [Aeq] is decidable. *)

Definition Aeqdec sitpn (x y : A sitpn) : {Aeq x y} + {~Aeq x y} :=
  P1SigEqdec Nat.eq_dec x y.
Arguments Aeqdec {sitpn}.

#[export] Hint Unfold Aeq Akeq Aeqdec : core.

(** For a given [sitpn], defines the equivalence relation [Feq]
    between two functions as the equality between the first element of
    the [sig] type [F sitpn].  *)

Definition Feq sitpn (f f' : F sitpn) : Prop := P1SigEq f f'.
Arguments Feq {sitpn}.

(** For a given [sitpn], defines the equivalence relation [Fkeq]
    between two pairs where functions are the first elements of the
    pairs.  *)

Definition Fkeq sitpn {B : Type} (p p' : F sitpn * B) : Prop := Feq (fst p) (fst p') /\ snd p = snd p'.

Arguments Fkeq {sitpn B}.

(** The equivalence relation [Feq] is decidable. *)

Definition Feqdec sitpn (x y : F sitpn) : {Feq x y} + {~Feq x y} :=
  P1SigEqdec Nat.eq_dec x y.
Arguments Feqdec {sitpn}.

#[export] Hint Unfold Feq Fkeq Feqdec : core.

(** For a given [sitpn], defines the equivalence relation [Ceq]
    between two conditions as the equality between the first element
    of the [sig] type [C sitpn].  *)

Definition Ceq sitpn (c c' : C sitpn) : Prop := P1SigEq c c'.
Arguments Ceq {sitpn}.

(** For a given [sitpn], defines the equivalence relation [Ckeq]
    between two pairs where conditions are the first elements of the
    pairs.  *)

Definition Ckeq sitpn {B : Type} (p p' : C sitpn * B) : Prop := Ceq (fst p) (fst p') /\ snd p = snd p'.

Arguments Ckeq {sitpn B}.

(** The equivalence relation [Ceq] is decidable. *)

Definition Ceqdec sitpn (x y : C sitpn) : {Ceq x y} + {~Ceq x y} :=
  P1SigEqdec Nat.eq_dec x y.
Arguments Ceqdec {sitpn}.

#[export] Hint Unfold Ceq Ckeq Ceqdec : core.

author: viampietro

repo: ver-hilecop

save_path: github-repos/coq/viampietro-ver-hilecop


text:
(** Generated by coq-of-ocaml *)
Require Import OCaml.OCaml.

Local Set Primitive Projections.
Local Open Scope string_scope.
Local Open Scope Z_scope.
Local Open Scope type_scope.
Import ListNotations.

Unset Positivity Checking.
Unset Guard Checking.

Inductive nat : Set :=
| O : nat
| S : nat -> nat.

Inductive natural : Set :=
| Zero : natural
| Succ : natural -> natural.

Fixpoint plus (plus_arg0 : natural) (plus_arg1 : natural) {struct plus_arg0}
  : natural :=
  match plus_arg0 with
  | Zero => plus_arg1
  | Succ n => Succ (plus n plus_arg1)
  end.

Fixpoint mult (mult_arg0 : natural) (mult_arg1 : natural) {struct mult_arg0}
  : natural :=
  match mult_arg0 with
  | Zero => Zero
  | Succ n => plus (mult n mult_arg1) mult_arg1
  end.

Definition synth (lf1 : natural) (x : natural) : natural :=
  mult lf1 (plus x Zero).

author: yalhessi

repo: lemmaranker

save_path: github-repos/coq/yalhessi-lemmaranker


text:
(* NEXT: ===> Cons                                                              *)

Require Import Logic.Set.Set.
Require Import Logic.Set.Incl.
Require Import Logic.Set.Elem.
Require Import Logic.Set.Trans.
Require Import Logic.Set.Equal.
Require Import Logic.Set.ToList.
Require Import Logic.Set.ElemIncl.

(* The extensionality axiom is one of the axioms of Zermelo-Fraenkel set theory *)
(* aka 'ZF'. It expresses the fact that two sets are equal if and only if they  *)
(* have identical elements. This axiom is true in our model. It is not obvious  *)
(* that this should be the case, as we have defined equality between sets as a  *)
(* stronger property than simply having identical elements. So this axiom is a  *)
(* strong result, and it is effectively saying there is no need to check that   *)
(* two sets belong to the same sets in order to establish their equality.       *)
(* The statement of extensionality is an axiom in standard set theory. But of   *)
(* course we are defining a model of set theory within Coq. So extensionality   *)
(* is not an axiom in this case. It is something we prove from the Coq logical  *)
(* system and our definitions of the type 'set' and the relations '::' and '==' *)
Theorem extensionality : forall (x y:set),
    x == y <-> forall (z:set), z :: x <-> z :: y.
Proof.
    intros x y. split.
    - intros [H1 H2]. assumption.
    - intros H. split.
        + assumption.
        + intros z. split; intros H'; apply toListElem in H'.
            { destruct H' as [x' [H1 [H2 H3]]].
              apply toListElem. exists x'. split.
                { assumption. }
                { split.
                    { apply inclTrans with x.
                        { apply elemIncl. apply H. }
                        { assumption. }}
                    { apply inclTrans with x.
                        { assumption. }
                        { apply elemIncl. apply H. }}}}
            { destruct H' as [y' [H1 [H2 H3]]].
              apply toListElem. exists y'. split.
                { assumption. }
                { split.
                    { apply inclTrans with y.
                        { apply elemIncl. apply H. }
                        { assumption. }}
                    { apply inclTrans with y.
                        { assumption. }
                        { apply elemIncl. apply H. }}}}
Qed.

(* A consequence of extensionality is that equality is equivalent to double     *)
(* inclusion. So while we were very careful to define equality in the proper    *)
(* way, in the end we have a notion which is no stronger than double inclusion. *)
Theorem doubleIncl : forall (x y:set),
    x == y <-> (x <= y) /\ (y <= x).
Proof.
    intros x y. split.
    - intros H. destruct H as [H1 H2]. split; apply elemIncl; apply H1.
    - intros [H1 H2]. apply extensionality. intros z. split; intros H.
        + rewrite elemIncl in H1. apply H1. assumption.
        + rewrite elemIncl in H2. apply H2. assumption.
Qed.

author: possientis

repo: Prog

save_path: github-repos/coq/possientis-Prog


text:
From Cdcl Require Import Itauto. #[local] Tactic Notation "itauto" := itauto auto.
From stdpp Require Import prelude fin_sets.
From AML Require Import Signature Pattern.

Section sec_variables.

Context
  `{signature}.

Inductive EVarFree (x : EVar) : Pattern -> Prop :=
| ef_evar : EVarFree x (PEVar x)
| ef_impl_left : forall ϕ ψ, EVarFree x ϕ -> EVarFree x (PImpl ϕ ψ)
| ef_impl_right : forall ϕ ψ, EVarFree x ψ -> EVarFree x (PImpl ϕ ψ)
| ef_app_left : forall ϕ ψ, EVarFree x ϕ -> EVarFree x (PApp ϕ ψ)
| ef_app_right : forall ϕ ψ, EVarFree x ψ -> EVarFree x (PApp ϕ ψ)
| ef_mu : forall X ϕ, EVarFree x ϕ -> EVarFree x (μₚ X ϕ)
| ef_ex : forall y ϕ, EVarFree x ϕ -> y <> x -> EVarFree x (PEx y ϕ)
.

Inductive EVarBound (x : EVar) : Pattern -> Prop :=
| eb_impl_left : forall ϕ ψ, EVarBound x ϕ -> EVarBound x (PImpl ϕ ψ)
| eb_impl_right : forall ϕ ψ, EVarBound x ψ -> EVarBound x (PImpl ϕ ψ)
| eb_app_left : forall ϕ ψ, EVarBound x ϕ -> EVarBound x (PApp ϕ ψ)
| eb_app_right : forall ϕ ψ, EVarBound x ψ -> EVarBound x (PApp ϕ ψ)
| eb_mu : forall X ϕ, EVarBound x ϕ -> EVarBound x (μₚ X ϕ)
| eb_ex_eq : forall ϕ, EVarBound x (PEx x ϕ)
| eb_ex_neq : forall y ϕ, EVarBound x ϕ -> EVarBound x (PEx y ϕ)
.

Inductive SVarFree (x : SVar) : Pattern -> Prop :=
| sf_svar : SVarFree x (PSVar x)
| sf_impl_left : forall ϕ ψ, SVarFree x ϕ -> SVarFree x (PImpl ϕ ψ)
| sf_impl_right : forall ϕ ψ, SVarFree x ψ -> SVarFree x (PImpl ϕ ψ)
| sf_app_left : forall ϕ ψ, SVarFree x ϕ -> SVarFree x (PApp ϕ ψ)
| sf_app_right : forall ϕ ψ, SVarFree x ψ -> SVarFree x (PApp ϕ ψ)
| sf_ex : forall X ϕ, SVarFree x ϕ -> SVarFree x (PEx X ϕ)
| sf_mu : forall y ϕ, SVarFree x ϕ -> y <> x -> SVarFree x (μₚ y ϕ)
.

Inductive SVarBound (x : SVar) : Pattern -> Prop :=
| sb_impl_left : forall ϕ ψ, SVarBound x ϕ -> SVarBound x (PImpl ϕ ψ)
| sb_impl_right : forall ϕ ψ, SVarBound x ψ -> SVarBound x (PImpl ϕ ψ)
| sb_app_left : forall ϕ ψ, SVarBound x ϕ -> SVarBound x (PApp ϕ ψ)
| sb_app_right : forall ϕ ψ, SVarBound x ψ -> SVarBound x (PApp ϕ ψ)
| sb_ex : forall X ϕ, SVarBound x ϕ -> SVarBound x (PEx X ϕ)
| sb_mu_eq : forall ϕ, SVarBound x (μₚ x ϕ)
| sb_mu_neq : forall y ϕ, SVarBound x ϕ -> SVarBound x (μₚ y ϕ)
.

Fixpoint FEV (p : Pattern) : EVarSet :=
match p with
| PEVar x => {[x]}
| PSVar X => ∅
| POp _ => ∅
| PImpl ϕ ψ => FEV ϕ ∪ FEV ψ
| PApp ϕ ψ => FEV ϕ ∪ FEV ψ
| PEx x ϕ => FEV ϕ ∖ {[x]}
| μₚ X ϕ => FEV ϕ
end.

Lemma EVarFree_FEV : forall x p,
EVarFree x p <-> x ∈ FEV p.
Proof.
induction p; cbn.
- by rewrite elem_of_singleton; split; inversion 1; constructor.
- by split; [inversion 1 | intro Hx; contradict Hx; apply not_elem_of_empty].
- rewrite elem_of_union, <- IHp1, <- IHp2.
  by split; [inversion 1; [left | right] | intros []; [apply ef_impl_left | apply ef_impl_right]].
- rewrite elem_of_difference, elem_of_singleton, <- IHp.
  by split; [inversion 1 | intros []; constructor].
- rewrite <- IHp.
  by split; [inversion 1 | constructor].
- rewrite elem_of_union, <- IHp1, <- IHp2.
  by split; [inversion 1; [left | right] | intros []; [apply ef_app_left | apply ef_app_right]].
- by split; [inversion 1 | intro Hx; contradict Hx; apply not_elem_of_empty].
Qed.

#[export] Instance EVarFree_dec : RelDecision EVarFree.
Proof.
by intros x p; destruct (elem_of_dec_slow x (FEV p)); [left | right];
  rewrite EVarFree_FEV.
Qed.

Fixpoint FSV (p : Pattern) : SVarSet :=
match p with
| PSVar x => {[x]}
| PEVar X => ∅
| POp _ => ∅
| PImpl ϕ ψ => FSV ϕ ∪ FSV ψ
| PApp ϕ ψ => FSV ϕ ∪ FSV ψ
| μₚ x ϕ => FSV ϕ ∖ {[x]}
| PEx X ϕ => FSV ϕ
end.

Lemma SVarFree_FSV : forall x p,
SVarFree x p <-> x ∈ FSV p.
Proof.
induction p; cbn.
- by split; [inversion 1 | intro Hx; contradict Hx; apply not_elem_of_empty].
- by rewrite elem_of_singleton; split; inversion 1; constructor.
- rewrite elem_of_union, <- IHp1, <- IHp2.
  by split; [inversion 1; [left | right] | intros []; [apply sf_impl_left | apply sf_impl_right]].
- rewrite <- IHp.
  by split; [inversion 1 | constructor].
- rewrite elem_of_difference, elem_of_singleton, <- IHp.
  by split; [inversion 1 | intros []; constructor].
- rewrite elem_of_union, <- IHp1, <- IHp2.
  by split; [inversion 1; [left | right] | intros []; [apply sf_app_left | apply sf_app_right]].
- by split; [inversion 1 | intro Hx; contradict Hx; apply not_elem_of_empty].
Qed.

#[export] Instance SVarFree_dec : RelDecision SVarFree.
Proof.
by intros x p; destruct (elem_of_dec_slow x (FSV p)); [left | right];
  rewrite SVarFree_FSV.
Qed.

Fixpoint BEV (p : Pattern) : EVarSet :=
match p with
| PEVar _ => ∅
| PSVar _ => ∅
| POp _ => ∅
| PImpl ϕ ψ => BEV ϕ ∪ BEV ψ
| PApp ϕ ψ => BEV ϕ ∪ BEV ψ
| PEx x ϕ => BEV ϕ ∪ {[x]}
| μₚ X ϕ => BEV ϕ
end.

Lemma EVarBound_BEV : forall x p,
EVarBound x p <-> x ∈ BEV p.
Proof.
induction p; cbn.
- by split; [inversion 1 | intro Hx; contradict Hx; apply not_elem_of_empty].
- by split; [inversion 1 | intro Hx; contradict Hx; apply not_elem_of_empty].
- rewrite elem_of_union, <- IHp1, <- IHp2.
  by split; [inversion 1; [left | right] | intros []; [apply eb_impl_left | apply eb_impl_right]].
- rewrite elem_of_union, elem_of_singleton, <- IHp.
  split; [by inversion 1; [right | left] |].
  destruct (decide (x = e)) as [-> |]; [by intros; apply eb_ex_eq |].
  by intros []; [apply eb_ex_neq |].
- rewrite <- IHp.
  by split; [inversion 1 | constructor].
- rewrite elem_of_union, <- IHp1, <- IHp2.
  by split; [inversion 1; [left | right] | intros []; [apply eb_app_left | apply eb_app_right]].
- by split; [inversion 1 | intro Hx; contradict Hx; apply not_elem_of_empty].
Qed.

#[export] Instance EVarBound_dec : RelDecision EVarBound.
Proof.
by intros x p; destruct (elem_of_dec_slow x (BEV p)); [left | right];
  rewrite EVarBound_BEV.
Qed.

Definition EV (p : Pattern) : EVarSet := FEV p ∪ BEV p.
Definition EOccurs (x : EVar) (p : Pattern) : Prop := EVarFree x p \/ EVarBound x p.

Lemma EV_Eoccurs : forall x p, EOccurs x p <-> x ∈ EV p.
Proof.
by intros; unfold EV; rewrite elem_of_union, <- EVarFree_FEV, <- EVarBound_BEV.
Qed.

Lemma EOccurs_impl x ϕ1 ϕ2 :
EOccurs x (PImpl ϕ1 ϕ2) <-> EOccurs x ϕ1 \/ EOccurs x ϕ2.
Proof.
rewrite EV_Eoccurs; unfold EV; cbn; rewrite! elem_of_union; unfold EOccurs.
rewrite !EVarFree_FEV, !EVarBound_BEV.
itauto.
Qed.

Lemma EOccurs_app x ϕ1 ϕ2 :
EOccurs x (PApp ϕ1 ϕ2) <-> EOccurs x ϕ1 \/ EOccurs x ϕ2.
Proof.
rewrite EV_Eoccurs; unfold EV; cbn; rewrite! elem_of_union.
unfold EOccurs; rewrite !EVarFree_FEV, !EVarBound_BEV.
itauto.
Qed.

Lemma EOccurs_ex x y ϕ :
EOccurs x (PEx y ϕ) <-> x = y \/ EOccurs x ϕ.
Proof.
rewrite EV_Eoccurs; unfold EV; cbn.
rewrite! elem_of_union, elem_of_difference, elem_of_singleton.
unfold EOccurs; rewrite !EVarFree_FEV, !EVarBound_BEV.
destruct (decide (x = y)); itauto.
Qed.

Lemma EOccurs_mu x Y ϕ :
EOccurs x (μₚ Y ϕ) <-> EOccurs x ϕ.
Proof.
rewrite EV_Eoccurs; unfold EV; cbn.
rewrite! elem_of_union.
unfold EOccurs; rewrite !EVarFree_FEV, !EVarBound_BEV.
itauto.
Qed.

Inductive EOccursInd (x : EVar) : Pattern -> Prop :=
| eo_evar : EOccursInd x (PEVar x)
| eo_impl_left : forall ϕ1 ϕ2, EOccursInd x ϕ1 -> EOccursInd x (PImpl ϕ1 ϕ2)
| eo_impl_right : forall ϕ1 ϕ2, EOccursInd x ϕ2 -> EOccursInd x (PImpl ϕ1 ϕ2)
| eo_app_left : forall ϕ1 ϕ2, EOccursInd x ϕ1 -> EOccursInd x (PApp ϕ1 ϕ2)
| eo_app_right : forall ϕ1 ϕ2, EOccursInd x ϕ2 -> EOccursInd x (PApp ϕ1 ϕ2)
| eo_mu : forall Y ϕ, EOccursInd x ϕ -> EOccursInd x (μₚ Y ϕ)
| eo_ex_eq : forall ϕ, EOccursInd x (PEx x ϕ)
| eo_ex_neq : forall y ϕ, EOccursInd x ϕ -> EOccursInd x (PEx y ϕ).

Lemma EOccursInd_iff x ϕ : EOccurs x ϕ <-> EOccursInd x ϕ.
Proof.
induction ϕ.
2,7: by split; [intros [Hx | Hx]; inversion Hx | inversion 1].
- by split; [intros [Hx | Hx]; inversion Hx | inversion 1; left ]; constructor.
- rewrite EOccurs_impl, IHϕ1, IHϕ2.
  by split; [intros []; constructor | inversion 1]; itauto.
- rewrite EOccurs_ex, IHϕ.
  split; [intros []; [subst; apply eo_ex_eq | apply eo_ex_neq] | inversion 1];
    itauto.
- rewrite EOccurs_mu, IHϕ.
  by split; [constructor | inversion 1].
- rewrite EOccurs_app, IHϕ1, IHϕ2.
  by split; [intros []; constructor | inversion 1]; itauto.
Qed.

Fixpoint BSV (p : Pattern) : SVarSet :=
match p with
| PEVar _ => ∅
| PSVar _ => ∅
| POp _ => ∅
| PImpl ϕ ψ => BSV ϕ ∪ BSV ψ
| PApp ϕ ψ => BSV ϕ ∪ BSV ψ
| μₚ x ϕ => BSV ϕ ∪ {[x]}
| PEx X ϕ => BSV ϕ
end.

Lemma SVarBound_BSV : forall x p,
SVarBound x p <-> x ∈ BSV p.
Proof.
induction p; cbn.
- by split; [inversion 1 | intro Hx; contradict Hx; apply not_elem_of_empty].
- by split; [inversion 1 | intro Hx; contradict Hx; apply not_elem_of_empty].
- rewrite elem_of_union, <- IHp1, <- IHp2.
  by split; [inversion 1; [left | right] | intros []; [apply sb_impl_left | apply sb_impl_right]].
- rewrite <- IHp.
  by split; [inversion 1 | constructor].
- rewrite elem_of_union, elem_of_singleton, <- IHp.
  split; [by inversion 1; [right | left] |].
  destruct (decide (x = s)) as [-> |]; [by intros; apply sb_mu_eq |].
  by intros []; [apply sb_mu_neq |].
- rewrite elem_of_union, <- IHp1, <- IHp2.
  by split; [inversion 1; [left | right] | intros []; [apply sb_app_left | apply sb_app_right]].
- by split; [inversion 1 | intro Hx; contradict Hx; apply not_elem_of_empty].
Qed.

#[export] Instance SVarBound_dec : RelDecision SVarBound.
Proof.
by intros x p; destruct (elem_of_dec_slow x (BSV p)); [left | right];
  rewrite SVarBound_BSV.
Qed.

Definition SV (p : Pattern) : SVarSet := FSV p ∪ BSV p.
Definition SOccurs (x : SVar) (p : Pattern) : Prop := SVarFree x p \/ SVarBound x p.

Lemma SV_Soccurs : forall x p, SOccurs x p <-> x ∈ SV p.
Proof.
by intros; unfold SV; rewrite elem_of_union, <- SVarFree_FSV, <- SVarBound_BSV.
Qed.

Lemma SOccurs_impl x ϕ1 ϕ2 :
SOccurs x (PImpl ϕ1 ϕ2) <-> SOccurs x ϕ1 \/ SOccurs x ϕ2.
Proof.
rewrite SV_Soccurs; unfold SV; cbn; rewrite! elem_of_union; unfold SOccurs.
rewrite !SVarFree_FSV, !SVarBound_BSV.
itauto.
Qed.

Lemma SOccurs_app x ϕ1 ϕ2 :
SOccurs x (PApp ϕ1 ϕ2) <-> SOccurs x ϕ1 \/ SOccurs x ϕ2.
Proof.
rewrite SV_Soccurs; unfold SV; cbn; rewrite! elem_of_union.
unfold SOccurs; rewrite !SVarFree_FSV, !SVarBound_BSV.
itauto.
Qed.

Lemma SOccurs_mu x y ϕ :
SOccurs x (μₚ y ϕ) <-> x = y \/ SOccurs x ϕ.
Proof.
rewrite SV_Soccurs; unfold SV; cbn.
rewrite! elem_of_union, elem_of_difference, elem_of_singleton.
unfold SOccurs; rewrite !SVarFree_FSV, !SVarBound_BSV.
destruct (decide (x = y)); itauto.
Qed.

Lemma SOccurs_ex x Y ϕ :
SOccurs x (PEx Y ϕ) <-> SOccurs x ϕ.
Proof.
rewrite SV_Soccurs; unfold SV; cbn.
rewrite! elem_of_union.
unfold SOccurs; rewrite !SVarFree_FSV, !SVarBound_BSV.
itauto.
Qed.

Inductive SOccursInd (x : SVar) : Pattern -> Prop :=
| so_svar : SOccursInd x (PSVar x)
| so_impl_left : forall ϕ1 ϕ2, SOccursInd x ϕ1 -> SOccursInd x (PImpl ϕ1 ϕ2)
| so_impl_right : forall ϕ1 ϕ2, SOccursInd x ϕ2 -> SOccursInd x (PImpl ϕ1 ϕ2)
| so_app_left : forall ϕ1 ϕ2, SOccursInd x ϕ1 -> SOccursInd x (PApp ϕ1 ϕ2)
| so_app_right : forall ϕ1 ϕ2, SOccursInd x ϕ2 -> SOccursInd x (PApp ϕ1 ϕ2)
| so_ex : forall Y ϕ, SOccursInd x ϕ -> SOccursInd x (PEx Y ϕ)
| so_mu_eq : forall ϕ, SOccursInd x (μₚ x ϕ)
| so_mu_neq : forall y ϕ, SOccursInd x ϕ -> SOccursInd x (μₚ y ϕ).

Lemma SOccursInd_iff x ϕ : SOccurs x ϕ <-> SOccursInd x ϕ.
Proof.
induction ϕ.
1,7: by split; [intros [Hx | Hx]; inversion Hx | inversion 1].
- by split; [intros [Hx | Hx]; inversion Hx | inversion 1; left ]; constructor.
- rewrite SOccurs_impl, IHϕ1, IHϕ2.
  by split; [intros []; constructor | inversion 1]; itauto.
- rewrite SOccurs_ex, IHϕ.
  by split; [constructor | inversion 1].
- rewrite SOccurs_mu, IHϕ.
  split; [intros []; [subst; apply so_mu_eq | apply so_mu_neq] | inversion 1];
    itauto.
- rewrite SOccurs_app, IHϕ1, IHϕ2.
  by split; [intros []; constructor | inversion 1]; itauto.
Qed.

Lemma SubPatternExBound z theta ϕ : SubPattern (PEx z theta) ϕ -> z ∈ BEV ϕ.
Proof.
  induction 1; cbn.
  - by cbn; rewrite elem_of_union, elem_of_singleton; right.
  - by apply elem_of_union; left.
  - by apply elem_of_union; right.
  - by apply elem_of_union; left.
  - by apply elem_of_union; right.
  - by apply elem_of_union; left.
  - done.
Qed.

Lemma SubPatternMuBound z theta ϕ : SubPattern (μₚ z theta) ϕ -> z ∈ BSV ϕ.
Proof.
  induction 1; cbn.
  - by cbn; rewrite elem_of_union, elem_of_singleton; right.
  - by apply elem_of_union; left.
  - by apply elem_of_union; right.
  - by apply elem_of_union; left.
  - by apply elem_of_union; right.
  - done.
  - by apply elem_of_union; left.
Qed.

Record EFreeFor (x : EVar) (delta ϕ : Pattern) :=
{
  eff_evar : forall z, EVarFree z delta -> z <> x ->
    forall theta, SubPattern (PEx z theta) ϕ -> ~ EVarFree x theta;
  eff_svar : forall z, SVarFree z delta ->
    forall theta, SubPattern (μₚ z theta) ϕ -> ~ EVarFree x theta
}.

Lemma EFreeForAtomic x delta a : PatternAtomic a -> EFreeFor x delta a.
Proof. by inversion 1; (split; [inversion 3 | inversion 2]). Qed.

Lemma EFreeForImpl x delta ϕ1 ϕ2 :
  EFreeFor x delta (PImpl ϕ1 ϕ2) <-> EFreeFor x delta ϕ1 /\ EFreeFor x delta ϕ2.
Proof.
  split; [intros [He Hs] | intros [[He1 Hs1] [He2 Hs2]]];
    [split |]; (split; intros z Hz; [intros Hxz|]; intros theta Hsub).
  - by eapply He; [..| apply sp_impl_left].
  - by eapply Hs; [| apply sp_impl_left].
  - by eapply He; [..| apply sp_impl_right].
  - by eapply Hs; [| apply sp_impl_right].
  - by inversion_clear Hsub; [eapply He1 | eapply He2].
  - by inversion_clear Hsub; [eapply Hs1 | eapply Hs2].
Qed.

Lemma EFreeForApp x delta ϕ1 ϕ2 :
  EFreeFor x delta (PApp ϕ1 ϕ2) <-> EFreeFor x delta ϕ1 /\ EFreeFor x delta ϕ2.
Proof.
  split; [intros [He Hs] | intros [[He1 Hs1] [He2 Hs2]]];
    [split |]; (split; intros z Hz; [intros Hxz|]; intros theta Hsub).
  - by eapply He; [..| apply sp_app_left].
  - by eapply Hs; [| apply sp_app_left].
  - by eapply He; [..| apply sp_app_right].
  - by eapply Hs; [| apply sp_app_right].
  - by inversion_clear Hsub; [eapply He1 | eapply He2].
  - by inversion_clear Hsub; [eapply Hs1 | eapply Hs2].
Qed.

Lemma EFreeForEx x delta y ϕ :
  EFreeFor x delta (PEx y ϕ) <-> EFreeFor x delta ϕ /\ (EVarFree y delta -> x <> y -> ~ EVarFree x ϕ).
Proof.
  split; [intros [He Hs] | intros [[He Hs] Hy]]; repeat split.
  - by intros; eapply He; [..| apply sp_ex].
  - by intros; eapply Hs; [| apply sp_ex].
  - by intros; eapply He; [.. | apply sp_refl].
  - by inversion 3; subst; [apply Hy | eapply He].
  - by inversion 2; subst; eapply Hs.
Qed.

Lemma EFreeForMu x delta y ϕ :
  EFreeFor x delta (μₚ y ϕ) <-> EFreeFor x delta ϕ /\ (SVarFree y delta -> ~ EVarFree x ϕ).
Proof.
  split; [intros [He Hs] | intros [[He Hs] Hy]]; repeat split.
  - by intros; eapply He; [..| apply sp_mu].
  - by intros; eapply Hs; [| apply sp_mu].
  - by intros; eapply Hs; [| apply sp_refl].
  - by inversion 3; subst; eapply He.
  - by inversion 2; subst; [apply Hy | eapply Hs].
Qed.

Inductive EFreeForInd (x : EVar) (delta : Pattern) : Pattern -> Prop :=
| effi_evar : forall y, EFreeForInd x delta (PEVar y)
| effi_svar : forall Y, EFreeForInd x delta (PSVar Y)
| effi_op : forall o, EFreeForInd x delta (POp o)
| effi_impl : forall ϕ1 ϕ2, EFreeForInd x delta ϕ1 -> EFreeForInd x delta ϕ2 ->
    EFreeForInd x delta (PImpl ϕ1 ϕ2)
| effi_app : forall ϕ1 ϕ2, EFreeForInd x delta ϕ1 -> EFreeForInd x delta ϕ2 ->
    EFreeForInd x delta (PApp ϕ1 ϕ2)
| effi_ex : forall y ϕ, EFreeForInd x delta ϕ -> (EVarFree y delta -> x <> y -> ~ EVarFree x ϕ) ->
    EFreeForInd x delta (PEx y ϕ)
| effi_mu : forall Y ϕ, EFreeForInd x delta ϕ -> (SVarFree Y delta -> ~ EVarFree x ϕ) ->
    EFreeForInd x delta (μₚ Y ϕ).

Lemma EFreeForInd_iff x delta ϕ : EFreeFor x delta ϕ <-> EFreeForInd x delta ϕ.
Proof.
  induction ϕ.
  1-2,7: by split; [constructor |split; [inversion 3 | inversion 2]].
  - rewrite EFreeForImpl, IHϕ1, IHϕ2.
    by split; [by intros []; constructor | inversion 1].
  - rewrite EFreeForEx, IHϕ.
    by split; [by intros []; constructor | inversion 1].
  - rewrite EFreeForMu, IHϕ.
    by split; [by intros []; constructor | inversion 1].
  - rewrite EFreeForApp, IHϕ1, IHϕ2.
    by split; [by intros []; constructor | inversion 1].
Qed.

Lemma EFreeForInd_x_not_occurs x delta ϕ (Hx : ~ EOccursInd x ϕ) : EFreeForInd x delta ϕ.
Proof.
  induction ϕ; cycle 4. 3-5 : by constructor.
  - constructor; [by apply IHϕ; contradict Hx; constructor |].
    by intros _; contradict Hx; constructor; apply EOccursInd_iff; left.
  - by constructor; [apply IHϕ1 | apply IHϕ2]; contradict Hx;
      [apply eo_app_left | apply eo_app_right].
  - by constructor; [apply IHϕ1 | apply IHϕ2]; contradict Hx;
      [apply eo_impl_left | apply eo_impl_right].
  - constructor; [by apply IHϕ; contradict Hx; constructor |].
    by intros _ _; contradict Hx; constructor; apply EOccursInd_iff; left.
Qed.

Lemma EFreeFor_x_theta_if_not_bound x theta ϕ :
  (forall y, EVarFree y theta -> y <> x -> ~ EVarBound y ϕ) ->
  (forall y, SVarFree y theta -> ~ SVarBound y ϕ) ->
  EFreeFor x theta ϕ.
Proof.
  intros Hetheta Hstheta; (split; intros z Hz; [intros Hzx |]; intros theta' Htheta'); exfalso.
  - by eapply Hetheta; [..| eapply EVarBound_BEV, SubPatternExBound].
  - by eapply Hstheta; [| eapply SVarBound_BSV, SubPatternMuBound].
Qed.

Lemma EFreeFor_x_theta_if_no_free_vars x theta ϕ :
  FEV theta ⊆ {[x]} ->
  FSV theta ≡ ∅ ->
  EFreeFor x theta ϕ.
Proof.
  intros Hetheta Hstheta; apply EFreeFor_x_theta_if_not_bound.
  - by intros y Hy; apply EVarFree_FEV, Hetheta, elem_of_singleton in Hy.
  - by intro; rewrite SVarFree_FSV, Hstheta; set_solver.
Qed.

Lemma EFreeFor_x_y_if_not_bound x y ϕ (Hx : ~ EVarBound y ϕ) : EFreeFor x (PEVar y) ϕ.
Proof. by apply EFreeFor_x_theta_if_not_bound; inversion 1. Qed.

Record SFreeFor (x : SVar) (delta ϕ : Pattern) :=
{
  sff_evar : forall z, EVarFree z delta ->
    forall theta, SubPattern (PEx z theta) ϕ -> ~ SVarFree x theta;
  sff_svar : forall z, SVarFree z delta -> z <> x ->
    forall theta, SubPattern (μₚ z theta) ϕ -> ~ SVarFree x theta
}.

Lemma SFreeForAtomic x delta a : PatternAtomic a -> SFreeFor x delta a.
Proof. by inversion 1; (split; [inversion 2 | inversion 3]). Qed.

Lemma SFreeForImpl x delta ϕ1 ϕ2 :
  SFreeFor x delta (PImpl ϕ1 ϕ2) <-> SFreeFor x delta ϕ1 /\ SFreeFor x delta ϕ2.
Proof.
  split; [intros [He Hs] | intros [[He1 Hs1] [He2 Hs2]]];
    [split |]; (split; intros z Hz; [| intros Hxz]; intros theta Hsub).
  - by eapply He; [| apply sp_impl_left].
  - by eapply Hs; [..| apply sp_impl_left].
  - by eapply He; [| apply sp_impl_right].
  - by eapply Hs; [..| apply sp_impl_right].
  - by inversion_clear Hsub; [eapply He1 | eapply He2].
  - by inversion_clear Hsub; [eapply Hs1 | eapply Hs2].
Qed.

Lemma SFreeForApp x delta ϕ1 ϕ2 :
  SFreeFor x delta (PApp ϕ1 ϕ2) <-> SFreeFor x delta ϕ1 /\ SFreeFor x delta ϕ2.
Proof.
  split; [intros [He Hs] | intros [[He1 Hs1] [He2 Hs2]]];
    [split |]; (split; intros z Hz; [| intros Hxz]; intros theta Hsub).
  - by eapply He; [| apply sp_app_left].
  - by eapply Hs; [..| apply sp_app_left].
  - by eapply He; [| apply sp_app_right].
  - by eapply Hs; [..| apply sp_app_right].
  - by inversion_clear Hsub; [eapply He1 | eapply He2].
  - by inversion_clear Hsub; [eapply Hs1 | eapply Hs2].
Qed.

Lemma SFreeForEx x delta y ϕ :
  SFreeFor x delta (PEx y ϕ) <-> SFreeFor x delta ϕ /\ (EVarFree y delta -> ~ SVarFree x ϕ).
Proof.
  split; [intros [He Hs] | intros [[He Hs] Hy]]; repeat split.
  - by intros; eapply He; [| apply sp_ex].
  - by intros; eapply Hs; [..| apply sp_ex].
  - by intros; eapply He; [| apply sp_refl].
  - by inversion 2; subst; [apply Hy | eapply He].
  - by inversion 3; subst; eapply Hs.
Qed.

Lemma SFreeForMu x delta y ϕ :
  SFreeFor x delta (μₚ y ϕ) <-> SFreeFor x delta ϕ /\ (SVarFree y delta -> y <> x -> ~ SVarFree x ϕ).
Proof.
  split; [intros [He Hs] | intros [[He Hs] Hy]]; repeat split.
  - by intros; eapply He; [| apply sp_mu].
  - by intros; eapply Hs; [..| apply sp_mu].
  - by intros; eapply Hs; [..| apply sp_refl].
  - by inversion 2; subst; eapply He.
  - by inversion 3; subst; [apply Hy | eapply Hs].
Qed.

Inductive SFreeForInd (x : SVar) (delta : Pattern) : Pattern -> Prop :=
| sffi_evar : forall y, SFreeForInd x delta (PEVar y)
| sffi_svar : forall Y, SFreeForInd x delta (PSVar Y)
| sffi_op : forall o, SFreeForInd x delta (POp o)
| sffi_impl : forall ϕ1 ϕ2, SFreeForInd x delta ϕ1 -> SFreeForInd x delta ϕ2 ->
    SFreeForInd x delta (PImpl ϕ1 ϕ2)
| sffi_app : forall ϕ1 ϕ2, SFreeForInd x delta ϕ1 -> SFreeForInd x delta ϕ2 ->
    SFreeForInd x delta (PApp ϕ1 ϕ2)
| sffi_ex : forall y ϕ, SFreeForInd x delta ϕ -> (EVarFree y delta -> ~ SVarFree x ϕ) ->
    SFreeForInd x delta (PEx y ϕ)
| sffi_mu : forall Y ϕ, SFreeForInd x delta ϕ -> (SVarFree Y delta -> Y <> x -> ~ SVarFree x ϕ) ->
    SFreeForInd x delta (μₚ Y ϕ).

Lemma SFreeForInd_iff x delta ϕ : SFreeFor x delta ϕ <-> SFreeForInd x delta ϕ.
Proof.
  induction ϕ.
  1-2,7: by split; [constructor | split; [inversion 2 | inversion 3]].
  - rewrite SFreeForImpl, IHϕ1, IHϕ2.
    by split; [by intros []; constructor | inversion 1].
  - rewrite SFreeForEx, IHϕ.
    by split; [by intros []; constructor | inversion 1].
  - rewrite SFreeForMu, IHϕ.
    by split; [intros []; constructor | inversion 1].
  - rewrite SFreeForApp, IHϕ1, IHϕ2.
    by split; [by intros []; constructor | inversion 1].
Qed.

Lemma SFreeForInd_x_not_occurs x delta ϕ (Hx : ~ SOccursInd x ϕ) : SFreeForInd x delta ϕ.
Proof.
  induction ϕ; cycle 4. 3-5 : by constructor.
  - constructor; [by apply IHϕ; contradict Hx; constructor |].
    by intros _ _; contradict Hx; constructor; apply SOccursInd_iff; left.
  - by constructor; [apply IHϕ1 | apply IHϕ2]; contradict Hx;
      [apply so_app_left | apply so_app_right].
  - by constructor; [apply IHϕ1 | apply IHϕ2]; contradict Hx;
      [apply so_impl_left | apply so_impl_right].
  - constructor; [by apply IHϕ; contradict Hx; constructor |].
    by intros _; contradict Hx; constructor; apply SOccursInd_iff; left.
Qed.

Lemma SFreeFor_x_theta_if_not_bound x theta ϕ :
  (forall y, EVarFree y theta -> ~ EVarBound y ϕ) ->
  (forall y, SVarFree y theta -> y <> x -> ~ SVarBound y ϕ) ->
  SFreeFor x theta ϕ.
Proof.
  intros Hetheta Hstheta; (split; intros z Hz; [| intros Hxz]; intros theta' Htheta'); exfalso.
  - by eapply Hetheta; [| eapply EVarBound_BEV, SubPatternExBound].
  - by eapply Hstheta; [..| eapply SVarBound_BSV, SubPatternMuBound].
Qed.

Lemma SFreeFor_x_theta_if_no_free_vars x theta ϕ :
  FEV theta ≡ ∅ ->
  FSV theta ⊆ {[x]} ->
  SFreeFor x theta ϕ.
Proof.
  intros Hetheta Hstheta; apply SFreeFor_x_theta_if_not_bound.
  - by intro; rewrite EVarFree_FEV, Hetheta; set_solver.
  - by intros y Hy; apply SVarFree_FSV, Hstheta, elem_of_singleton in Hy.
Qed.

Lemma SFreeFor_x_y_if_not_bound x y ϕ (Hx : ~ SVarBound y ϕ) : SFreeFor x (PSVar y) ϕ.
Proof. by apply SFreeFor_x_theta_if_not_bound; inversion 1. Qed.

Inductive OccursPositively (X : SVar) : Pattern -> Prop :=
| op_evar : forall x, OccursPositively X (PEVar x)
| op_svar : forall Y, OccursPositively X (PSVar Y)
| op_cons : forall c, OccursPositively X (POp c)
| op_app : forall ϕ ψ, OccursPositively X ϕ -> OccursPositively X ψ ->
    OccursPositively X (PApp ϕ ψ)
| op_ex : forall x ϕ, OccursPositively X ϕ -> OccursPositively X (PEx x ϕ)
| op_mu_eq : forall ϕ, OccursPositively X (μₚ X ϕ)
| op_mu_neq : forall Y ϕ, Y <> X -> OccursPositively X ϕ ->
    OccursPositively X (μₚ Y ϕ)
| op_impl : forall ϕ ψ, OccursNegatively X ϕ -> OccursPositively X ψ ->
    OccursPositively X (PImpl ϕ ψ)
with OccursNegatively (X : SVar) : Pattern -> Prop :=
| on_evar : forall x, OccursNegatively X (PEVar x)
| on_svar : forall Y, Y <> X -> OccursNegatively X (PSVar Y)
| on_cons : forall c, OccursNegatively X (POp c)
| on_app : forall ϕ ψ, OccursNegatively X ϕ -> OccursNegatively X ψ ->
    OccursNegatively X (PApp ϕ ψ)
| on_ex : forall x ϕ, OccursNegatively X ϕ -> OccursNegatively X (PEx x ϕ)
| on_mu_eq : forall ϕ, OccursNegatively X (μₚ X ϕ)
| on_mu_neq : forall Y ϕ, Y <> X -> OccursNegatively X ϕ ->
    OccursNegatively X (μₚ Y ϕ)
| on_impl : forall ϕ ψ, OccursPositively X ϕ -> OccursNegatively X ψ ->
    OccursNegatively X (PImpl ϕ ψ)
.

Record ClosedPattern (ϕ : Pattern) : Prop :=
{
  cpe : forall x, ~ EVarFree x ϕ;
  cps : forall X, ~ SVarFree X ϕ;
}.

Definition set_closed_pattern `{Set_ Pattern PatternSet} (Gamma : PatternSet) : Prop :=
  forall ϕ, ϕ ∈ Gamma -> ClosedPattern ϕ.

Lemma ClosedPattern_iff ϕ :
  ClosedPattern ϕ <-> FEV ϕ ≡ ∅ /\ FSV ϕ ≡ ∅.
Proof.
  split; intros [HEV HSV]; cycle 1; split.
  - by intros x Hx; rewrite EVarFree_FEV, HEV in Hx; contradict Hx; apply not_elem_of_empty.
  - by intros x Hx; rewrite SVarFree_FSV, HSV in Hx; contradict Hx; apply not_elem_of_empty.
  - intro x; specialize (HEV x).
    rewrite EVarFree_FEV in HEV.
    by set_solver.
  - intro x; specialize (HSV x).
    rewrite SVarFree_FSV in HSV.
    by set_solver.
Qed.

Lemma ClosedPattern_elim ϕ :
  FEV ϕ ≡ ∅ -> FSV ϕ ≡ ∅ -> ClosedPattern ϕ.
Proof. by intros; apply ClosedPattern_iff. Qed.

Definition CFEV (c : AppContext) : EVarSet := FEV (csubst c pBot).

Lemma elem_of_CFEV x c : x ∈ CFEV c <-> forall ϕ, x ∈ FEV (csubst c ϕ).
Proof.
  split; [| by intros Hϕ; apply Hϕ].
  induction c; cbn; [intros Hx; contradict Hx; apply not_elem_of_empty |..];
    setoid_rewrite elem_of_union; intros [] ϕ.
  - by left; apply IHc.
  - by right.
  - by left.
  - by right; apply IHc.
Qed.

Inductive CEVarFree (x : EVar) : AppContext -> Prop :=
| cevf_ll : forall c p, CEVarFree x c -> CEVarFree x (LApp c p)
| cevf_lr : forall c p, EVarFree x p -> CEVarFree x (LApp c p)
| cevf_rr : forall c p, CEVarFree x c -> CEVarFree x (RApp p c)
| cevf_rl : forall c p, EVarFree x p -> CEVarFree x (RApp p c)
.

Lemma CEVarFree_CFEV x c : CEVarFree x c <-> x ∈ CFEV c.
Proof.
  induction c; cbn.
  - by split; [inversion 1 | intros Hx; contradict Hx; apply not_elem_of_empty].
  - rewrite elem_of_union, <- IHc.
    split; [inversion 1 | intros []]; subst.
    + by left.
    + by right; apply EVarFree_FEV.
    + by apply cevf_ll.
    + by apply cevf_lr; apply EVarFree_FEV.
  - rewrite elem_of_union, <- IHc.
    split; [inversion 1 | intros []]; subst.
    + by right.
    + by left; apply EVarFree_FEV.
    + by apply cevf_rl; apply EVarFree_FEV.
    + by apply cevf_rr.
Qed.

End sec_variables.

author: traiansf

repo: aml-in-coq

save_path: github-repos/coq/traiansf-aml-in-coq


text:
Require Import ListAux.
Require Import TreeAux.
Require Import Tactics.
Lemma customstk3consistent_top0 (il_0:list nat) (i_0:nat) (u_0:nat) (u_1:nat) : (top_spec  il_0 i_0) -> (((u_0 = i_0)/\(u_1 = u_0)/\(list_member  il_0 u_1)) -> (list_head  il_0 i_0)).
Proof. solve_top; try (assert (u_0 = u_1); subst; eauto). Qed.

Lemma customstk3consistent_top1 (il_0:list nat) (i_0:nat) (u_0:nat) (u_1:nat) : (top_spec  il_0 i_0) -> (((not (u_0 = i_0))/\(u_1 = u_0)/\(list_member  il_0 u_1)) -> (not (list_head  il_0 u_0))).
Proof. solve_top; try (assert (u_0 = u_1); subst; eauto). Qed.

Lemma customstk3consistent_top2 (il_0:list nat) (i_0:nat) (u_0:nat) (u_1:nat) : (top_spec  il_0 i_0) -> (((u_1 = i_0)/\(not (u_1 = u_0))/\(list_member  il_0 u_1)) -> (list_head  il_0 i_0)).
Proof. solve_top; try (assert (u_0 = u_1); subst; eauto). Qed.

Lemma customstk3consistent_top3 (il_0:list nat) (i_0:nat) (u_0:nat) (u_1:nat) : (top_spec  il_0 i_0) -> (((u_1 = i_0)/\(not (u_1 = u_0))/\(list_member  il_0 u_1)) -> (not (list_head  il_0 u_0))).
Proof. solve_top; try (assert (u_0 = u_1); subst; eauto). Qed.

Lemma customstk3consistent_top4 (il_0:list nat) (i_0:nat) (u_0:nat) (u_1:nat) : (top_spec  il_0 i_0) -> (((list_member  il_0 u_0)/\(u_1 = i_0)/\(not (u_1 = u_0))/\(list_member  il_0 u_1)) -> (list_order  il_0 i_0 u_0)).
Proof. solve_top; try (assert (u_0 = u_1); subst; eauto). Qed.

Lemma customstk3consistent_top5 (il_0:list nat) (i_0:nat) (u_0:nat) (u_1:nat) : (top_spec  il_0 i_0) -> (((not (list_member  il_0 u_0))/\(u_1 = i_0)/\(not (u_1 = u_0))/\(list_member  il_0 u_1)) -> (not (list_order  il_0 i_0 u_0))).
Proof.
    intro pushspec;
  inversion pushspec as [a b Hhd]; subst; intros; destruct_pairs;
  try (match goal with
       | x: nat, y: nat, z: nat |- _ => destruct (Hhd x); destruct (Hhd y); destruct (Hhd z)
       | x: nat, y: nat |- _ => destruct (Hhd x); destruct (Hhd y)
       | x: nat |- _ => destruct (Hhd x)
       end). eauto.
Qed.

Lemma customstk3consistent_top6 (il_0:list nat) (i_0:nat) (u_0:nat) (u_1:nat) : (top_spec  il_0 i_0) -> (((not (list_member  il_0 u_0))/\(u_1 = i_0)/\(not (u_1 = u_0))/\(list_member  il_0 u_1)) -> (not (list_order  il_0 u_0 i_0))).
Proof.
    intro pushspec;
      inversion pushspec as [a b Hhd]; subst; intros; try intr_not; destruct_pairs.
    eauto.
Qed.

Lemma customstk3consistent_top7 (il_0:list nat) (i_0:nat) (u_0:nat) (u_1:nat) : (top_spec  il_0 i_0) -> (((not (u_1 = i_0))/\(not (u_1 = u_0))/\(list_member  il_0 u_1)) -> (not (list_head  il_0 u_1))).
Proof. solve_top; try (assert (u_0 = u_1); subst; eauto). Qed.

Lemma customstk3consistent_top8 (il_0:list nat) (i_0:nat) (u_0:nat) (u_1:nat) : (top_spec  il_0 i_0) -> (((list_member  il_0 u_0)/\(u_0 = i_0)/\(not (u_1 = i_0))/\(not (u_1 = u_0))/\(list_member  il_0 u_1)) -> (list_head  il_0 i_0)).
Proof. solve_top; try (assert (u_0 = u_1); subst; eauto). Qed.

Lemma customstk3consistent_top9 (il_0:list nat) (i_0:nat) (u_0:nat) (u_1:nat) : (top_spec  il_0 i_0) -> (((list_member  il_0 u_0)/\(u_0 = i_0)/\(not (u_1 = i_0))/\(not (u_1 = u_0))/\(list_member  il_0 u_1)) -> (list_order  il_0 i_0 u_1)).
Proof. solve_top; try (assert (u_0 = u_1); subst; eauto). Qed.

Lemma customstk3consistent_top10 (il_0:list nat) (i_0:nat) (u_0:nat) (u_1:nat) : (top_spec  il_0 i_0) -> (((list_member  il_0 u_0)/\(not (u_0 = i_0))/\(not (u_1 = i_0))/\(not (u_1 = u_0))/\(list_member  il_0 u_1)) -> (not (list_head  il_0 u_0))).
Proof. solve_top; try (assert (u_0 = u_1); subst; eauto). Qed.

Lemma customstk3consistent_top11 (il_0:list nat) (i_0:nat) (u_0:nat) (u_1:nat) : (top_spec  il_0 i_0) -> (((not (list_member  il_0 u_1))) -> (not (u_1 = i_0))).
Proof. solve_top; try (assert (u_0 = u_1); subst; eauto). Qed.

Lemma customstk3consistent_top12 (il_0:list nat) (i_0:nat) (u_0:nat) (u_1:nat) : (top_spec  il_0 i_0) -> (((not (list_member  il_0 u_1))) -> (not (list_order  il_0 u_1 u_0))).
Proof. intros. intro.
       eauto. Qed.

Lemma customstk3consistent_top13 (il_0:list nat) (i_0:nat) (u_0:nat) (u_1:nat) : (top_spec  il_0 i_0) -> (((u_0 = i_0)/\(not (list_member  il_0 u_1))) -> (list_member  il_0 i_0)).
Proof. solve_top; try (assert (u_0 = u_1); subst; eauto). Qed.

Lemma customstk3consistent_top14 (il_0:list nat) (i_0:nat) (u_0:nat) (u_1:nat) : (top_spec  il_0 i_0) -> (((u_0 = i_0)/\(not (list_member  il_0 u_1))) -> (list_head  il_0 i_0)).
Proof. solve_top; try (assert (u_0 = u_1); subst; eauto). Qed.

Lemma customstk3consistent_top15 (il_0:list nat) (i_0:nat) (u_0:nat) (u_1:nat) : (top_spec  il_0 i_0) -> (((u_0 = i_0)/\(not (list_member  il_0 u_1))) -> (not (list_order  il_0 i_0 u_1))).
Proof. intros. intro. destruct H0. eauto. Qed.

author: zhezhouzz


text:
(* eh, i already know how to use option for the most part *)

Require Import Nat.
Require Import List.

Variable A : Type.

Fixpoint nth_error (l : list nat) (n : nat) : option nat :=
  match l with
  | nil => None
  | h::t => match eqb h n with
            | true => Some h
            | false => nth_error t (pred n)
            end
  end.

Compute (nth_error (1::2::3::4::nil) 2).

repo: Coq-Work


text:
(*========================================================================*)
(*                                                                        *)
(*                    CompcertTSO                                         *)
(*                                                                        *)
(*          Jaroslav Sevcik, University of Cambridge                      *)
(*          Viktor Vafeiadis, University of Cambridge                     *)
(*          Francesco Zappa Nardelli, INRIA Rocquencourt                  *)
(*          Suresh Jagannathan, Purdue University                         *)
(*          Peter Sewell, University of Cambridge                         *)
(*                                                                        *)
(*          (building on CompCert 1.5 and a 1.8 pre-release)              *)
(*                                                                        *)
(*  This document and the CompCertTSO sources are copyright 2005, 2006,   *)
(*  2007, 2008, 2009, 2010, 2011 Institut National de Recherche en        *)
(*  Informatique et en Automatique (INRIA), and Suresh Jagannathan,       *)
(*  Jaroslav Sevcik, Peter Sewell and Viktor Vafeiadis.                   *)
(*                                                                        *)
(*  All rights reserved.  This file is distributed under the terms of     *)
(*  the INRIA Non-Commercial License Agreement.                           *)
(*                                                                        *)
(*                                                                        *)
(*                                                                        *)
(*                                                                        *)
(*                                                                        *)
(*========================================================================*)

(** This file contains additional properties about memories. *)

Require Import Coqlib.
Require Import Integers.
Require Import Values.
Require Import Pointers.
Require Import Mem.
Require Import Ast.
Require Import Maps.
Require Import Libtactics.

Set Implicit Arguments.

(*----------------------------------------------------------------------------*)
(** * Basic lemmata *)
(*----------------------------------------------------------------------------*)

Lemma store_allocated:
  forall {p c v m m'} (A: store_ptr c m p v = Some m') r k,
  range_allocated r k m' <-> range_allocated r k m.
Proof.
  by intros; eapply iff_sym, (store_preserves_allocated_ranges A).
Qed.

Lemma alloc_allocated:
  forall {r' k' m m'} (A: alloc_ptr r' k' m = Some m') r k,
  range_allocated r k m' <-> range_allocated r k m \/ (r = r' /\ k = k').
Proof.
  split; intro; des; clarify.
  - eapply (alloc_preserves_allocated_back A) in H; tauto.
  - by apply (alloc_preserves_allocated A).
  - by destruct (alloc_someD A).
Qed.

Lemma free_allocated:
  forall {p k' m m' n}
    (F: free_ptr p k' m = Some m')
    (RA: range_allocated (p,n) k' m) r k,
  range_allocated r k m' <-> range_allocated r k m /\ fst r <> p.
Proof.
  split; intro; des.
    split; [eby eapply (free_preserves_allocated_back F)|].
    eby intro; clarify; destruct r; eapply free_not_allocated.
  eapply (free_preserves_allocated F) in H; des; clarify.
Qed.

Lemma load_alloc_inside2 :
  forall {r k m m' c' p'},
    alloc_ptr r k m = Some m' ->
    range_inside (range_of_chunk p' c') r ->
    load_ptr c' m' p' =
      (if pointer_chunk_aligned_dec p' c' then Some Vundef else None).
Proof.
  intros; destruct (pointer_chunk_aligned_dec p' c').
  - eby eapply load_alloc_inside.
  destruct (load_ptr c' m' p') as [] _eqn: X; try done.
  by destruct (load_chunk_allocated_someD X).
Qed.

Lemma load_alloc_not_inside2 :
  forall {r k m m' c' p'},
    alloc_ptr r k m = Some m' ->
    load_ptr c' m p' = None ->
    ~ range_inside (range_of_chunk p' c') r ->
    load_ptr c' m' p' = None.
Proof.
  intros; destruct (ranges_disjoint_dec (range_of_chunk p' c') r).
    by rewrite (load_alloc_other H).
  by rewrite (load_alloc_overlap H).
Qed.

Lemma load_free_none :
  forall {p k m m' c' p'},
    free_ptr p k m = Some m' ->
    load_ptr c' m p' = None ->
    load_ptr c' m' p' = None.
Proof.
  intros; destruct (free_someD H) as [n RA].
  destruct (ranges_disjoint_dec (range_of_chunk p' c') (p, n)).
    eby erewrite (load_free_other H).
  eby erewrite (load_free_overlap H).
Qed.

Lemma load_store_none :
  forall {p c v m m' c' p'},
    store_ptr c m p v = Some m' ->
    load_ptr c' m p' = None ->
    load_ptr c' m' p' = None.
Proof.
  intros; destruct (load_ptr c' m' p') as [] _eqn: X; clarify.
  destruct (load_chunk_allocated_someD X) as [(? & ? & ? & RA) ?].
  eapply (store_allocated H) in RA.
  eby destruct (load_chunk_allocated_noneD H0); repeat eexists.
Qed.

(*----------------------------------------------------------------------------*)
(** * Extensional equality on memories *)
(*----------------------------------------------------------------------------*)

Definition mem_eq m1 m2:=
   (forall chunk p, load_ptr chunk m1 p = load_ptr chunk m2 p)
/\ (forall r k, range_allocated r k m1 <-> range_allocated r k m2)
/\ (mrestr m1 = mrestr m2).

Lemma in_block1:
  forall lbnd hbnd l h k ba,
  alloclist_hbound lbnd (mkmobj l h k :: ba) = Some hbnd ->
  0 < lbnd ->
  hbnd <= Int.modulus ->
  valid_access Mint8unsigned (l mod Int.modulus) (mkmobj l h k :: ba).
Proof.
  intros; constructor 1 with (k:=k); [|by apply Zone_divide].
  exists l; exists h; split; [by left|].
  exploit (@alloclist_hbound_impl_l_lt_h); [eassumption|by left|intro].
  rewrite Zmod_small; simpl; omega.
Qed.

Lemma alloclist1:
  forall lbnd hbnd l h k a,
  alloclist_hbound lbnd (mkmobj l h k :: a) = Some hbnd ->
  lbnd <= l /\ l < h /\ h <= hbnd /\ (align_size (h - l) | l).
Proof.
  intros lbnd hbnd l h k a H.
  by destruct (alloclist_hbound_impl_l_lt_h H (in_eq _ _)) as (? & ? & ? & ?).
Qed.

Lemma range_allocated_al_cons:
  forall l h k l' h' k' ba',
  range_allocated_al l h k (mkmobj l' h' k' :: ba') ->
  l = l' /\ h = h' /\ k = k' \/ range_allocated_al l h k ba'.
Proof.
  unfold range_allocated_al.
  by inversion 1; clarify; [left|right].
Qed.

Lemma valid_access_bounded:
  forall c ofs al lbnd hbnd,
   alloclist_hbound lbnd al = Some hbnd ->
   valid_access c ofs al ->
   lbnd <= ofs < hbnd.
Proof.
  intros until 0; intros H [k [l [h [RA ?]]] AL].
  eapply @alloclist_hbound_impl_l_lt_h in H; try edone.
  destruct c; simpl in *; omega.
Qed.

Lemma Zabs_nat_of_nat: forall n, Zabs_nat (Z_of_nat n) = n.
Proof.
  by destruct n; simpl; auto using nat_of_P_o_P_of_succ_nat_eq_succ.
Qed.

Lemma contents_eq_ext:
  forall bc bc' ba,
    block_valid (mkblock bc ba) ->
    block_valid (mkblock bc' ba) ->
    (forall c ofs,
      valid_access c ofs ba ->
      Val.load_result c (getN (pred_size_chunk c) (ofs mod Int.modulus) bc)
      = Val.load_result c (getN (pred_size_chunk c) (ofs mod Int.modulus) bc')) ->
  bc = bc'.
Proof.
  intros bc bc' ba (UU & OK & hbnd & B & M) (UU' & OK' & hbnd' & B' & M') LD.
  apply ZTree.ext; intros ofs.
  destruct (ZTree.get ofs bc) as [[]|] _eqn: G.

  Case "Datum".
    pose proof (proj1 (proj2 OK _ _ _ G)) as [c [SZ [VOK ACCOK]]].
    generalize (LD c ofs ACCOK).
    assert (ofsRNG: 0 <= ofs < Int.modulus)
      by (pose proof (valid_access_bounded _ B ACCOK); omega).
    rewrite Zmod_small; try done.
    destruct ACCOK as [k ? ?]; simpl in *.

    unfold getN.
    rewrite G, SZ, dec_eq_true, value_chunk_ok1; try done.
    destruct (ZTree.get ofs bc') as [[]|] _eqn: G'; try done; try destruct eq_nat_dec;
    try rewrite load_result_undef; intro X; clarify; try by revert VOK; clear; destruct c.

    pose proof (proj1 (proj2 OK' _ _ _ G')) as [c' [SZ' [VOK' ACCOK']]].
    rewrite value_chunk_ok1; try done.
    by revert VOK VOK' SZ'; clear; destruct c'; destruct c; destruct v0.

  Case "Cont".
    pose proof (proj1 OK _ _ G) as (l & v & Gm).
    pose proof (proj1 (proj2 OK _ _ _ Gm)) as [c [SZ [VOK ACCOK]]].
    generalize (LD _ _ ACCOK).
    assert (ofsRNG: 0 <= ofs - Z_of_nat n < Int.modulus)
      by (pose proof (valid_access_bounded _ B ACCOK); omega).
    rewrite Zmod_small; try done.
    destruct ACCOK as [k ? ?]; simpl in *.
    unfold getN.
    rewrite Gm, SZ, dec_eq_true, value_chunk_ok1; try done.
    destruct (ZTree.get (ofs - Z_of_nat n) bc') as [[]|] _eqn: G'; try done; try destruct eq_nat_dec;
    try rewrite load_result_undef; intro X; clarify; try by revert VOK; clear; destruct c.
    destruct n.
      by simpl in *; rewrite Zminus_0_r in *; rewrite G in Gm.

    pose proof (proj1 (proj2 OK' _ _ _ G')) as [c' [SZ' [VOK' ACCOK']]].
    exploit (check_cont_inside _ _ _ _ ofs (proj2 (proj2 OK' _ _ _ G')));
      unfold contents; rewrite inj_S.
    omega.
    intros ->; f_equal; f_equal.
    replace (ofs - (ofs - Zsucc (Z_of_nat n) + 1)) with (Z_of_nat n); [rewrite Zabs_nat_of_nat|]; omega.

  Case "None".
    destruct (ZTree.get ofs bc') as [[]|] _eqn: G'; try done.

    SCase "Datum".
      pose proof (proj1 (proj2 OK' _ _ _ G')) as [c [SZ [VOK ACCOK]]].
      generalize (LD c ofs ACCOK).
      assert (ofsRNG: 0 <= ofs < Int.modulus)
        by (pose proof (valid_access_bounded _ B ACCOK); omega).
      rewrite Zmod_small; try done.
      destruct ACCOK as [k ? ?]; simpl in *.
      unfold getN.
      rewrite G, G', SZ, dec_eq_true, load_result_undef, value_chunk_ok1; try done.
      by revert VOK; clear; destruct c; destruct v.

    SCase "Cont".
      pose proof (proj1 OK' _ _ G') as (l & v & Gm').
      pose proof (proj1 (proj2 OK' _ _ _ Gm')) as [c [SZ [VOK ACCOK]]].
      generalize (LD _ _ ACCOK).
      assert (ofsRNG: 0 <= ofs - Z_of_nat n < Int.modulus)
        by (pose proof (valid_access_bounded _ B ACCOK); omega).
      rewrite Zmod_small; try done.
      destruct ACCOK as [k ? ?]; simpl in *.
      unfold getN.
      rewrite Gm', SZ, dec_eq_true.
      destruct (ZTree.get (ofs - Z_of_nat n) bc) as [[]|] _eqn: Gm; try done; try destruct eq_nat_dec;
      try rewrite load_result_undef; try (by revert VOK; destruct c; destruct v).
      intro X; clarify.
      destruct n.
        by simpl in *; rewrite Zminus_0_r in *; rewrite G in Gm.

      pose proof (proj1 (proj2 OK _ _ _ Gm)) as [c' [SZ' [VOK' ACCOK']]].
      exploit (check_cont_inside _ _ _ _ ofs (proj2 (proj2 OK _ _ _ Gm)));
        unfold contents; rewrite inj_S.
      omega.
      by rewrite G.
Qed.

Lemma range_allocated_implies_allocs_eq:
  forall m m' b bc bc',
  (forall (r : arange) (k : mobject_kind), range_allocated r k m  <-> range_allocated r k m') ->
  ZTree.get b (mcont m) = Some bc ->
  ZTree.get b (mcont m') = Some bc' ->
  allocs bc = allocs bc'.
Proof.
  intros [mc mr mv] [mc' mr' mv'] b [bc ba] [bc' ba'] RA EQ EQ'; simpl in *.
  pose proof (proj2 (proj2 (proj1 (proj2 (proj2 mv _ _ EQ))))) as [hbnd [B M]].
  pose proof (proj2 (proj2 (proj1 (proj2 (proj2 mv' _ _ EQ'))))) as [hbnd' [B' M']].
  unfold range_allocated in *; simpl in *.

    assert (Y: forall ofs s k,
           range_allocated_al (Int.unsigned ofs)
              (Int.unsigned ofs + Int.unsigned s) k ba <->
            range_allocated_al (Int.unsigned ofs)
              (Int.unsigned ofs + Int.unsigned s) k ba').
      by intros; generalize (RA (Ptr b ofs, s) k); simpl; rewrite EQ, EQ'.
    clear RA; revert Y.
    simpl in *.
    clear EQ' EQ.
    revert B B' M'; cut (1 > 0); [|omega]; generalize 1 as lbnd; revert ba' hbnd'.

    induction ba as [|[l h k] ba IH]; destruct ba' as [|[l' h' k'] ba']; try done;
    intros hbnd' lbnd POS B B' M' Y.
    (*1*)
      exploit (proj2 (Y (Int.repr l') (Int.repr (h' - l')) k')); try done.
      apply alloclist1 in B'.
      left; simpl; f_equal; rewrite ?Zmod_small; omega.
    (*2*)
      exploit (proj1 (Y (Int.repr l) (Int.repr (h - l)) k)); try done.
      apply alloclist1 in B.
      left; simpl; f_equal; rewrite ?Zmod_small; omega.
    (* Main case *)
    assert (l = l' /\ h = h' /\ k = k') as [-> [-> ->]].
      pose proof (alloclist1 _ _ _ _ _ B).
      pose proof (alloclist1 _ _ _ _ _ B').
      exploit (proj1 (Y (Int.repr l) (Int.repr (h - l)) k)); simpl;
        rewrite ?Zmod_small, Zplus_minus; try omega; [by left|].
      exploit (proj2 (Y (Int.repr l') (Int.repr (h' - l')) k')); simpl;
        rewrite ?Zmod_small, Zplus_minus; try omega; [by left|].
      intros X' X.
      apply range_allocated_al_cons in X; destruct X as [X|X]; try done.
      apply range_allocated_al_cons in X'; destruct X' as [[-> [-> ->]]|X']; try done.
      simpl in B; destruct aligned_rng_dec; try done; destruct Z_le_dec; try done.
      simpl in B'; destruct aligned_rng_dec; try done; destruct Z_le_dec; try done.
      pose proof (alloclist_hbound_impl_l_lt_h B' X).
      pose proof (alloclist_hbound_impl_l_lt_h B X').
      omegaContradiction.
    f_equal.
    simpl in B, B'; destruct aligned_rng_dec; clarify; destruct Z_le_dec; clarify.
    apply IH with (hbnd' := hbnd') (lbnd := h'); try done.
      omega.
    intros ofs s k.
    split; intro IN.
      destruct (proj1 (Y ofs s k) (or_intror _ IN)) as [|]; clarify.
      pose proof (alloclist_hbound_impl_l_lt_h B IN).
      omegaContradiction.
    destruct (proj2 (Y ofs s k) (or_intror _ IN)) as [|]; clarify.
    pose proof (alloclist_hbound_impl_l_lt_h B' IN).
    omegaContradiction.
Qed.

Theorem mem_eq_ext:
  forall m1 m2, mem_eq m1 m2 -> m1 = m2.
Proof.
  intros [mc mr mv] [mc' mr' mv'] [LD [RA MR]]; simpl in *; subst mr'.
  cut (mc = mc'); [by intro; subst mc'; rewrite (proof_irrelevance _ mv mv')|].
  apply ZTree.ext; intros b.
  destruct (ZTree.get b mc) as [[bc ba]|] _eqn: EQ;
  destruct (ZTree.get b mc') as [[bc' ba']|] _eqn: EQ'; try done.

  Case "SomeSome".
  generalize (range_allocated_implies_allocs_eq _ _ _ RA EQ EQ'); simpl; intros <-.
  f_equal; f_equal.
  pose proof (proj1 (proj2 (proj2 mv _ _ EQ))) as V.
  pose proof (proj1 (proj2 (proj2 mv' _ _ EQ'))) as V'.
  apply (contents_eq_ext V V'); intros c ofs VA.
  generalize (LD c (Ptr b (Int.repr ofs))).
  simpl; unfold load; simpl; rewrite EQ, EQ'; simpl.
  rewrite Zmod_small, !in_block_true; try done.
    by intro; clarify.
  by destruct V as (? & ? & ? & B & ?);
     pose proof (valid_access_bounded _ B VA); omega.

  Case "SomeNone".
  case mv; intros _ V.
  pose proof (proj2 (V _ _ EQ)) as [[V1 [_ [hbnd [? ?]]]] M].
  destruct ba as [|[l h k] ?].
    assert (bc = ZTree.empty _); [|by elim M; subst].
    apply ZTree.ext; intro x; rewrite ZTree.gempty; apply V1; simpl.
    by intros k [? [? [RA' _]]]; inversion RA'.
  generalize (LD Mint8unsigned (Ptr b (Int.repr l))); unfold load_ptr, load;
  simpl; rewrite EQ, EQ'; simpl.
  eby rewrite in_block_empty, in_block_true; [|eapply in_block1].

  Case "NoneSome".
  case mv'; intros _ V.
  pose proof (proj2 (V _ _ EQ')) as [[V1 [_ [hbnd [? ?]]]] M].
  destruct ba' as [|[l h k] ?].
    assert (bc' = ZTree.empty _); [|by elim M; subst].
    apply ZTree.ext; intro x; rewrite ZTree.gempty; apply V1; simpl.
    by intros k [? [? [RA' _]]]; inversion RA'.
  generalize (LD Mint8unsigned (Ptr b (Int.repr l))); unfold load_ptr, load;
  simpl; rewrite EQ, EQ'; simpl.
  eby rewrite in_block_empty, in_block_true; [|eapply in_block1].
Qed.

(*----------------------------------------------------------------------------*)
(** * Load equality on memories *)
(*----------------------------------------------------------------------------*)

Lemma load_eq_preserved_by_store:
  forall {c m mx p c' p' v' m' mx'}
    (Leq: load_ptr c m p = load_ptr c mx p)
    (ST: store_ptr c' m  p' v' = Some m')
    (STx: store_ptr c' mx p' v' = Some mx'),
  load_ptr c m' p = load_ptr c mx' p.
Proof.
  intros.
  pose proof (load_chunk_allocated_spec c m p) as LDAL.
  pose proof (load_chunk_allocated_spec c mx p) as LDALX.
  pose proof (load_chunk_allocated_spec c m' p) as LDAL'.
  pose proof (load_chunk_allocated_spec c mx' p) as LDALX'.
  destruct (load_ptr c m p) as [v|] _eqn : SMLD.
    (* Load SUCCESS *)
    destruct (range_eq_dec (range_of_chunk p' c') (range_of_chunk p c))
      as [RCeq | RCneq].
      (* Reading exactly the memory written by the unbuffered store *)
      injection RCeq.
      intro SCeqm.
      assert (SCeq: size_chunk c' = size_chunk c).
      destruct c; destruct c'; simpl in *; compute in SCeqm; done.
      intro Peq; subst.
      by rewrite (load_store_similar ST SCeq), (load_store_similar STx SCeq).
    (* Reading from different memory; two cases: *)
    destruct (ranges_disjoint_dec (range_of_chunk p' c')
                                         (range_of_chunk p c))
        as [RDISJ | ROVER].
      (* Ranges completely disjoint *)
      rewrite <- (load_store_other ST RDISJ), SMLD.
      by rewrite <- (load_store_other STx RDISJ).
      (* Ranges overlap *)
      apply (store_preserves_chunk_allocation ST _ _) in LDAL.
      rewrite (load_store_overlap ST ROVER RCneq LDAL).
      destruct (load_ptr c mx p) as [v''|] _eqn : SMLD'.
      apply (store_preserves_chunk_allocation STx p c) in LDALX.
      rewrite (load_store_overlap STx ROVER RCneq LDALX).
      done.
      by destruct (load_ptr c mx' p);
        [apply (store_preserves_chunk_allocation STx _ _) in LDALX'|].
    (* Load FAIL *)
    apply sym_eq in Leq. rewrite Leq in LDALX.
    destruct (load_ptr c m' p) as [cmv|] _eqn : E2;
      destruct (load_ptr c mx' p) as [cmv'|] _eqn : E3;
        try apply (store_preserves_chunk_allocation STx _ _) in LDALX';
          try apply (store_preserves_chunk_allocation ST _ _) in LDAL';
            try done.
Qed.

Lemma load_eq_preserved_by_alloc:
  forall {c m mx p r' k' m' mx'}
    (Leq: load_ptr c m p = load_ptr c mx p)
    (AP: alloc_ptr r' k' m = Some m')
    (APx: alloc_ptr r' k' mx = Some mx'),
  load_ptr c m' p = load_ptr c mx' p.
Proof.
  intros; destruct r' as [p' n'].
  pose proof (load_chunk_allocated_spec c m p) as LDAL.
  pose proof (load_chunk_allocated_spec c mx p) as LDALX.
  pose proof (load_chunk_allocated_spec c m' p) as LDAL'.
  pose proof (load_chunk_allocated_spec c mx' p) as LDALX'.
  destruct (pointer_chunk_aligned_dec p c) as [CA | CNA].
    2: destruct (load_ptr c m' p); destruct (load_ptr c mx' p);
      try done; destruct LDAL'; destruct LDALX'; done.
  destruct (range_inside_dec (range_of_chunk p c) (p', n')) as [RI | RNI].
    (* loads inside the newly allocated region *)
    rewrite (load_alloc_inside AP); try done;
      rewrite (load_alloc_inside APx); done.
  destruct (ranges_disjoint_dec (range_of_chunk p c)
                                       (p', n')) as [DISJ | OVER].
    (* loads outside *)
    rewrite (load_alloc_other AP); try done;
      rewrite (load_alloc_other APx); done.
  (* loads overlap *)
  destruct (alloc_someD AP) as [APA _].
  destruct (alloc_someD APx) as [APA' _].
  destruct (load_ptr c m' p).
    destruct LDAL' as [[r [k [RI RA]]] _].
    destruct (ranges_are_disjoint RA APA) as [[-> ->] | DISJ]; try done.
    eby elim OVER; eapply disjoint_inside_disjoint.
  destruct (load_ptr c mx' p); try done.
  destruct LDALX' as [[r [k [RI RA]]] _].
  destruct (ranges_are_disjoint RA APA') as [[-> ->] | DISJ]; try done.
  eby elim OVER; eapply disjoint_inside_disjoint.
Qed.

Lemma load_eq_preserved_by_free_same_size:
  forall {c m mx p p' n' k' m' mx'}
    (Leq: load_ptr c m p = load_ptr c mx p)
    (RA: range_allocated (p', n') k' m)
    (FP: free_ptr p' k' m = Some m')
    (RAx: range_allocated (p', n') k' mx)
    (FPx: free_ptr p' k' mx = Some mx'),
  load_ptr c m' p = load_ptr c mx' p.
Proof.
  intros.
  destruct (ranges_disjoint_dec (range_of_chunk p c)
                                       (p', n')) as [DISJ | OVER].
    by rewrite (load_free_other FP RA DISJ),
               (load_free_other FPx RAx DISJ).
  by rewrite (load_free_overlap FP RA OVER),
             (load_free_overlap FPx RAx OVER).
Qed.

Lemma load_eq_preserved_by_free_diff_block:
  forall {c m mx p p' k' m' mx'}
    (Leq: load_ptr c m p = load_ptr c mx p)
    (DB: MPtr.block p <> MPtr.block p')
    (FP: free_ptr p' k' m = Some m')
    (FPx: free_ptr p' k' mx = Some mx'),
  load_ptr c m' p = load_ptr c mx' p.
Proof.
  intros.
  destruct (free_someD FP) as [n RA].
  destruct (free_someD FPx) as [nx RAx].
  rewrite (load_free_other FP RA);
    [|by destruct p; destruct p'; simpl in *; left].
  by rewrite (load_free_other FPx RAx);
    [|by destruct p; destruct p'; simpl in *; left].
Qed.

(*----------------------------------------------------------------------------*)
(** * Commutativity properties of memory operations *)
(*----------------------------------------------------------------------------*)

(** Allocation commutes over successful stores *)

Lemma alloc_comm_store:
  forall p c v r k m m1 m2 m'
    (A : alloc_ptr r k m = Some m1)
    (B1: store_ptr c m1 p v = Some m')
    (B2: store_ptr c m p v = Some m2),
  alloc_ptr r k m2 = Some m'.
Proof.
  intros.
  pose proof (alloc_someD A) as (? & ? & ? & HA).
  destruct (ranges_disjoint_dec (range_of_chunk p c) r) as [DISJ|OVER].
  2: by destruct (store_chunk_allocated_someD B2) as [(? & ? & ? & RA) _];
        edestruct HA; try eapply RA; eapply ranges_overlap_comm;
        eby intro; destruct OVER; eapply disjoint_inside_disjoint.

  destruct (alloc_ptr r k m2) as [] _eqn: D; clarify.
  2: by destruct (alloc_noneD D) as [|[|(? & ? & RO & RA)]]; clarify;
        [by destruct r as [[]]; simpl in *; rewrite (restr_of_store B2) in *
        |eby eapply (store_allocated B2) in RA; edestruct HA].

  f_equal; eapply mem_eq_ext; red.
  rewrite (restr_of_store B1), (restr_of_alloc D),
          (restr_of_store B2), (restr_of_alloc A).
  split; [|split]; try done.
  Case "load_eq".
  intros c' p'.
  destruct (range_inside_dec (range_of_chunk p' c') r) as [RI | RNI].
    rewrite (load_alloc_inside2 D RI); try done.
    rewrite <- (load_store_other B1); try done.
    2: eby eapply disjoint_inside_disjoint_r.
    by rewrite (load_alloc_inside2 A RI).
  destruct (ranges_disjoint_dec (range_of_chunk p' c') r) as [DISJ'| OVER].
    rewrite (load_alloc_other D DISJ').
    eapply load_eq_preserved_by_store; try eassumption.
    by rewrite (load_alloc_other A DISJ').
  rewrite (load_alloc_overlap D RNI OVER); symmetry.
  rewrite (load_store_none B1); try edone.
  eby eapply (load_alloc_overlap A).
  Case "ralloc".
  intros.
  eapply iff_trans, iff_sym, (store_allocated B1).
  eapply iff_trans, iff_sym, (alloc_allocated A).
  eapply iff_trans; [eapply (alloc_allocated D)|].
  by eapply or_iff_compat_r, (store_allocated B2).
Qed.

(** Allocation commutes over successful allocations *)

Lemma alloc_comm_alloc:
  forall r k r' k' m m1 m2 m'
    (A : alloc_ptr r k m = Some m1)
    (B1: alloc_ptr r' k' m1 = Some m')
    (B2: alloc_ptr r' k' m = Some m2),
  alloc_ptr r k m2 = Some m'.
Proof.
  intros.
  pose proof (alloc_someD A) as (? & ? & ? & HA).
  pose proof (alloc_someD B1) as (? & ? & ? & HB1); des.
  pose proof (alloc_someD B2) as (? & ? & ? & HB2); des.
  destruct (alloc_ptr r k m2) as [] _eqn: D; clarify.
  Case "some".
  pose proof (alloc_someD D) as (? & _ & _ & HD); des.
  f_equal; eapply mem_eq_ext; red.
  rewrite (restr_of_alloc B1), (restr_of_alloc D),
          (restr_of_alloc B2), (restr_of_alloc A).
  repeat split;
    try (by intro X; do 2 (
            eapply alloc_preserves_allocated_back in X; try edone;
            destruct X as [[? ?]|X]; clarify;
            eauto using @alloc_preserves_allocated)); [].
  destruct (ranges_disjoint_dec r r') as [DISJ|]; [|eby edestruct HD].
  intros c' p'.
  destruct (range_inside_dec (range_of_chunk p' c') r) as [RI | RNI].
    rewrite (load_alloc_inside2 D RI); try done.
    rewrite (load_alloc_other B1); try done.
    2: eby eapply disjoint_inside_disjoint.
    by rewrite (load_alloc_inside2 A RI).
  destruct (ranges_disjoint_dec (range_of_chunk p' c') r) as [DISJ'| OVER].
    rewrite (load_alloc_other D DISJ').
    eapply load_eq_preserved_by_alloc; try eassumption.
    by rewrite (load_alloc_other A DISJ').
  rewrite (load_alloc_overlap D RNI OVER); symmetry.

  destruct (load_ptr c' m' p') as [] _eqn: X; clarify.
  destruct (load_chunk_allocated_someD X) as [(? & ? & ? & ?) ?].
  destruct (load_chunk_allocated_noneD (load_alloc_overlap A RNI OVER)).
  eapply alloc_preserves_allocated_back in H10; try edone.
  des; split; vauto.
  eby destruct OVER; eapply ranges_disjoint_comm, disjoint_inside_disjoint_r.

  Case "none".
  pose proof (alloc_noneD D) as [|[|(r'' & k'' & RO & RA)]]; clarify.
  - by destruct r as [[]]; destruct r' as [[]]; simpl in *;
       rewrite (restr_of_alloc B2) in *.
  destruct (alloc_preserves_allocated_back B2 _ _ RA); des; clarify.
  - eby edestruct HB1; try eapply ranges_overlap_comm.
  eby edestruct HA.
Qed.

(** Allocation commutes over successful frees *)

Lemma alloc_comm_free:
  forall r k p k' m m1 m2 m'
    (A : alloc_ptr r k m = Some m1)
    (B1: free_ptr p k' m1 = Some m')
    (B2: free_ptr p k' m = Some m2),
  alloc_ptr r k m2 = Some m'.
Proof.
  intros.
  pose proof (alloc_someD A) as (? & ? & ? & HA).
  pose proof (free_someD B1) as (n1 & HB1); des.
  pose proof (free_someD B2) as (n2 & HB2); des.
  destruct (alloc_preserves_allocated_back A _ _ HB1) as [[]|]; clarify.
  - edestruct HA; try edone.
    by eapply non_empty_same_ptr_overlap;
       eauto using @valid_alloc_range_non_empty, @allocated_range_valid.
  destruct (alloc_ranges_same HB2 H2) as [? _]; clarify.
  destruct (ranges_disjoint_dec r (p, n1)) as [DISJ|]; [|eby edestruct HA].
  clear H2.
  destruct (alloc_ptr r k m2) as [] _eqn: D; clarify.

  Case "some".
  pose proof (alloc_someD D) as (? & _ & _ & HD); des.
  f_equal; eapply mem_eq_ext; red.
  rewrite (restr_of_free B1), (restr_of_alloc D),
          (restr_of_free B2), (restr_of_alloc A).
  split; [|split]; try done.
  SCase "load_eq".
  intros c' p'.
  destruct (range_inside_dec (range_of_chunk p' c') r) as [RI | RNI].
    rewrite (load_alloc_inside2 D RI); try done.
    erewrite (load_free_other B1); try edone.
    2: eby eapply disjoint_inside_disjoint.
    by rewrite (load_alloc_inside2 A RI).
  destruct (ranges_disjoint_dec (range_of_chunk p' c') r) as [DISJ'| OVER].
    rewrite (load_alloc_other D DISJ').
    eapply load_eq_preserved_by_free_same_size; try eapply B1; try eapply B2; try eassumption.
    by rewrite (load_alloc_other A DISJ').
  rewrite (load_alloc_overlap D RNI OVER); symmetry.
  destruct (load_ptr c' m' p') as [] _eqn: X; clarify.
  destruct (load_chunk_allocated_someD X) as [(? & ? & ? & RA) ?].
  eapply free_preserves_allocated_back in RA; try edone.
  destruct (load_chunk_allocated_noneD (load_alloc_overlap A RNI OVER)).
  by split; vauto.
  SCase "ralloc".
  intros.
  eapply iff_trans, iff_sym, (free_allocated B1); try edone.
  eapply iff_trans, iff_sym, and_iff_compat_r, (alloc_allocated A).
  eapply iff_trans; [eapply (alloc_allocated D)|].
  eapply iff_trans; [eby eapply or_iff_compat_r; eapply (free_allocated B2)|].
  destruct r0; split; intro; des; clarify; vauto.
  split; vauto; simpl; intro; clarify.
  edestruct HA; try edone.
  by eapply non_empty_same_ptr_overlap;
     eauto using @valid_alloc_range_non_empty, @allocated_range_valid.

  Case "none".
  pose proof (alloc_noneD D) as [|[[]|(r'' & k'' & RO & RA)]]; clarify.
  - by destruct r as [[]]; destruct p; simpl; rewrite (restr_of_free B2).
  pose proof (free_preserves_allocated_back B2 _ _ RA); des; clarify.
  eby edestruct HA.
Qed.

(** Free commutes over successful stores *)

Lemma free_comm_store:
  forall p c v r k m m1 m2 m'
    (A : free_ptr r k m = Some m1)
    (B1: store_ptr c m1 p v = Some m')
    (B2: store_ptr c m p v = Some m2),
  free_ptr r k m2 = Some m'.
Proof.
  intros.
  pose proof (free_someD A) as (n & RA).
  destruct (store_chunk_allocated_someD B1) as [(rr & k' & RI & RA1) _].
  destruct (free_ptr r k m2) as [m''|] _eqn: D; clarify.
  2: eby eapply (store_allocated B2) in RA; edestruct (free_noneD D).
  f_equal; eapply mem_eq_ext; red.
  rewrite (restr_of_store B1), (restr_of_free D),
          (restr_of_store B2), (restr_of_free A).
  split; [|split]; try done.
  Case "load_eq".
  destruct (ranges_are_disjoint RA (free_preserves_allocated_back A _ _ RA1)) as [[]|DISJ].
  + eby clarify; edestruct (free_not_allocated A).
  intros c' p'.
  destruct (ranges_disjoint_dec (range_of_chunk p' c')
                                       (r, n)) as [DISJ' | OVER].
    erewrite (load_free_other D); try edone; try eby eapply store_allocated.
    eapply load_eq_preserved_by_store; try eassumption.
    eby erewrite (load_free_other A).
  erewrite (load_free_overlap D); try edone; try eby eapply store_allocated.
  rewrite (load_store_none B1); try edone.
  eby eapply (load_free_overlap A).
  Case "ralloc".
  intros.
  eapply iff_trans, iff_sym, (store_allocated B1).
  eapply iff_trans, iff_sym, (free_allocated A RA).
  eapply iff_trans, and_iff_compat_r, (store_allocated B2).
  eby eapply (free_allocated D), (store_allocated B2).
Qed.

(** Free commutes over successful allocations *)

Lemma free_comm_alloc:
  forall p k r k' m m1 m2 m'
    (A : free_ptr p k m = Some m1)
    (B1: alloc_ptr r k' m1 = Some m')
    (B2: alloc_ptr r k' m = Some m2),
  free_ptr p k m2 = Some m'.
Proof.
  intros.
  pose proof (free_someD A) as (n & pRA).
  pose proof (alloc_someD B1) as (RA' & _ & _ & HB1).
  pose proof (alloc_someD B2) as (RA2 & _ & _ & HB).
  destruct (free_ptr p k m2) as [m''|] _eqn: D; clarify.
  2: eby edestruct (free_noneD D); eapply alloc_preserves_allocated.
  f_equal; eapply mem_eq_ext; red.
  rewrite (restr_of_alloc B1), (restr_of_free D),
          (restr_of_alloc B2), (restr_of_free A).
  split; [|split]; try done.
  Case "load_eq".
  intros c' p'.
  destruct (ranges_disjoint_dec (range_of_chunk p' c') (p, n)) as [DISJ' | OVER].
    erewrite (load_free_other D); try edone; try eby eapply alloc_preserves_allocated.
    eapply load_eq_preserved_by_alloc; try eassumption.
    eby erewrite (load_free_other A).
  erewrite (load_free_overlap D); try edone; try eby eapply alloc_preserves_allocated.
  erewrite load_alloc_not_inside2; try edone.
    eby erewrite (load_free_overlap A).
  intro.
  destruct OVER.
  eapply disjoint_inside_disjoint; try edone.
  edestruct (ranges_are_disjoint RA2 (alloc_preserves_allocated B2 _ _ pRA)) as [[]|];
    clarify.
  edestruct HB; try edone.
  by eapply non_empty_same_ptr_overlap;
     eauto using @valid_alloc_range_non_empty, @allocated_range_valid.
  Case "ralloc".
  intros.
  eapply iff_trans, iff_sym, (alloc_allocated B1); try done.
  eapply iff_trans, iff_sym, or_iff_compat_r, (free_allocated A pRA); try done.
  eapply iff_trans.
    eapply (free_allocated D); try edone; try eby eapply alloc_preserves_allocated.
  eapply iff_trans; [eby eapply and_iff_compat_r; eapply (alloc_allocated B2)|].
  split; intro; des; clarify; vauto.
  split; vauto; intro; clarify.
  destruct r; edestruct HB; try edone.
  by eapply non_empty_same_ptr_overlap;
     eauto using @valid_alloc_range_non_empty, @allocated_range_valid.
Qed.

(** Free commutes over successful frees *)

Lemma free_comm_free:
  forall p k p' k' m m1 m2 m'
    (A : free_ptr p k m = Some m1)
    (B1: free_ptr p' k' m1 = Some m')
    (B2: free_ptr p' k' m = Some m2),
  free_ptr p k m2 = Some m'.
Proof.
  intros.
  pose proof (free_someD A) as (n & pRA).
  pose proof (free_someD B1) as (n' & RA').
  assert (NEQ: p <> p') by (intro; clarify; apply (free_not_allocated A _ _ RA')).
  destruct (free_preserves_allocated B2 _ _ pRA); des; clarify.
  destruct (free_ptr p k m2) as [m''|] _eqn: D.
  2: eby edestruct (free_noneD D).
  f_equal; eapply mem_eq_ext; red.
  rewrite (restr_of_free B1), (restr_of_free D),
          (restr_of_free B2), (restr_of_free A).
  split; [|split]; try done.
  Case "load_eq".
  intros c' p''.
  destruct (ranges_disjoint_dec (range_of_chunk p'' c') (p, n)) as [DISJ' | OVER].
    erewrite (load_free_other D); try edone; try eby eapply alloc_preserves_allocated.
    eapply (load_eq_preserved_by_free_same_size); try eapply B1; try eapply B2; try eassumption.
    - eby erewrite (load_free_other A).
    eby eapply free_preserves_allocated_back in RA'.
  erewrite (load_free_overlap D); try edone.
  rewrite (load_free_none B1); try edone.
  eby erewrite (load_free_overlap A).
  Case "ralloc".
  intros.
  eapply iff_trans, iff_sym, (free_allocated B1); try edone.
  eapply iff_trans, iff_sym, and_iff_compat_r, (free_allocated A pRA); try done.
  eapply iff_trans; [eby eapply (free_allocated D)|].
  eapply iff_trans; [eby eapply and_iff_compat_r; eapply (free_allocated B2);
                         eapply (free_preserves_allocated_back A _ _ RA')|].
  tauto.
Qed.

(*----------------------------------------------------------------------------*)
(** ** Simple corollaries *)
(*----------------------------------------------------------------------------*)

Lemma alloc_comm_alloc_none:
  forall r k r' k' m m1 m2
    (A : alloc_ptr r k m = Some m1)
    (B : alloc_ptr r' k' m1 = None)
    (C : alloc_ptr r' k' m = Some m2),
    alloc_ptr r k m2 = None.
Proof.
  intros; destruct (alloc_ptr r k m2) as [] _eqn: D; clarify.
  eby erewrite alloc_comm_alloc in B.
Qed.

Lemma store_comm_alloc:
  forall r k c p v m m1 m2
    (A : store_ptr c m p v = Some m1)
    (B : alloc_ptr r k m1 = Some m2),
    exists m', alloc_ptr r k m = Some m' /\ store_ptr c m' p v = Some m2.
Proof.
  intros; destruct (alloc_ptr r k m) as [m'|] _eqn: C; clarify.
  - repeat eexists; try edone.
    destruct (store_ptr c m' p v) as [] _eqn: D.
    + eby erewrite alloc_comm_store in B.
    destruct (store_chunk_allocated_someD A) as [(?&?&?&?)?].
    destruct (store_chunk_allocated_noneD D); repeat eexists; try edone.
    eby eapply alloc_preserves_allocated.
  destruct (alloc_someD B) as (? & ? & ? & BB).
  destruct (alloc_noneD C); des; clarify.
  - by destruct r as [[]]; simpl in *; rewrite (restr_of_store A) in *.
  eby edestruct BB; try edone; eapply (store_allocated A).
Qed.

Lemma free_comm_store2:
  forall r k c p v m m1 m2
    (A : free_ptr r k m = Some m1)
    (B : store_ptr c m1 p v = Some m2),
    exists m', store_ptr c m p v = Some m' /\ free_ptr r k m' = Some m2.
Proof.
  intros; destruct (store_ptr c m p v) as [m'|] _eqn: C; clarify.
  - eby repeat eexists; try edone; eapply free_comm_store.
  destruct (store_chunk_allocated_someD B) as [(?&?&?&?)?].
  destruct (store_chunk_allocated_noneD C); repeat eexists; try edone.
  eby eapply (free_preserves_allocated_back A).
Qed.

author: shenghaoyuan

repo: CompCertTSO