text:
Require Import List String Arith.
Require Import mymatrices syntax context substitution.
Set Implicit Arguments.

Fixpoint aux_expand_fun (A : type) (N : intro_term) : intro_term :=
  match N with
  | ElimTerm K =>
    match A with
    | Matrix _ _ | Nat | Bool => ElimTerm K
    | Unit => TT
    | Computation P x A' Q =>
      let M := aux_expand_fun A' (Var x) in
      Dia (Let dia x <- K in M)
    end
  | _ => N
  end.

Inductive aux_reduce :
          (*input*) type -> intro_term -> var -> computation ->
          (*output*) computation -> Prop :=
| arElim : forall A K x E, aux_reduce A (ElimTerm K) x E (Let dia x <- K in E)
| arDia : forall A F x E E',
  monadic_subst F x (getShape A) E E' ->
  aux_reduce A (Dia F) x E E'
.

(* mem and init heaps are heap variables but are used continuously as heaps *)
Definition mem := HVar "mem".
Definition init := HVar "init".
Definition mem_context : heap_context := "mem"::nil.
Definition init_mem_context : heap_context := "init"::"mem"::nil.
Definition mem_init_context : heap_context := "mem"::"init"::nil.

(* This sequencing operator on propositions asserts that there is
   some heap in P which is the initial heap in Q *)
Definition seq_prop (P Q : proposition)(h : heap_var) : proposition :=
           ExistsHeap h (And (prop_subst "mem" (HVar h) P)
                             (prop_subst "init" (HVar h) Q)).
Notation "P / h \ Q" := (seq_prop P Q h) (at level 40).
Check (Top /"x"\ Bottom).

(* Strongest postcondition for select commands *)
Inductive sp : (*input*) command ->
               (*output*) proposition -> Prop :=
| spAlloc   : forall x A M P,
              P = And (HId mem (HUpdate init (Var x) M A))
                      (Not (Indom init (Var x))) ->
              sp (Alloc x M A) P
| spDealloc:  forall x A M P y,
              P = And (HId init (HUpdate mem (Var x) M A))
                 (And (Not (Indom mem (Var x)))
                      (seleq A init M (aux_expand_fun A (Var x)) y)) ->
              sp (Dealloc x M A) P
| spLookup : forall x A M P y,
              P = And (HId mem init)
                      (seleq A mem M (aux_expand_fun A (Var x)) y) ->
              sp (Lookup x M A) P
| dpMutate  : forall A M N P,
              P = HId (HVar "mem") (HUpdate (HVar "init") M N A) ->
              sp (Mutate M N A) P
.
Hint Constructors sp.

Definition sp_alloc x M A : proposition := And (HId mem (HUpdate init (Var x) M A))
                                               (Not (Indom init (Var x))).
Lemma sp_sp_alloc : forall x A M, sp (Alloc x M A) (sp_alloc x M A).
  intros; auto.
Qed.
Definition sp_lookup x M A y := And (HId mem init)
                                    (seleq A mem M (aux_expand_fun A (Var x)) y).
Lemma sp_sp_lookup : forall x M A y, sp (Lookup x M A) (sp_lookup x M A y).
  intros; eapply spLookup; reflexivity.
Qed.
Definition sp_dealloc x M A y := And (HId init (HUpdate mem (Var x) M A))
                                (And (Not (Indom mem (Var x)))
                                     (seleq A init M (aux_expand_fun A (Var x)) y)).
Lemma sp_sp_dealloc : forall x M A y, sp (Dealloc x M A) (sp_dealloc x M A y).
  intros; eapply spDealloc; reflexivity.
Qed.
Definition sp_mutate M N A := HId mem (HUpdate init M N A).
Lemma sp_sp_mutate : forall M N A, sp (Mutate M N A) (sp_mutate M N A).
  intros; auto.
Qed.

Section typing.

  (* Coercion from propositions to singleton prop contexts *)
  Definition singletonProp (P : proposition) : prop_context := P::nil.
  Coercion singletonProp : proposition >-> prop_context.

(* A variable context is well-formed if all the types in the context
   are canonical *)

Inductive wf_var_context : var_context -> Prop :=
| wfNil  : wf_var_context nil
| wfCons : forall x A VC,
           wf_var_context VC ->
           check_type VC A A -> (*A is canonical*)
           wf_var_context ((x,A)::VC)
| wfTail : forall x y A B VC,
           wf_var_context ((x,A)::VC) ->
           wf_var_context ((y,B)::VC) ->
           free_in_type y A = false ->
           wf_var_context ((x,A)::(y,B)::VC)

(* A proposition context is well_formed if all the propositions in the
   context are canonical *)
with wf_prop_context : var_context -> heap_context -> prop_context -> Prop :=
| wfpNil  : forall VC HC,
            wf_var_context VC ->
            wf_prop_context VC HC nil
| wfpCons : forall P VC HC PC,
            wf_prop_context VC HC PC ->
            check_prop VC HC P P (* P is canonical *) ->
            wf_prop_context VC HC (P::PC)

with check_type :
     (*input*) var_context -> type ->
     (*output*) type -> Prop :=
| ctUnit   : forall VC,
           wf_var_context VC ->
           check_type VC Unit Unit
| ctBool   : forall VC,
           wf_var_context VC ->
           check_type VC Bool Bool
| ctNat    : forall VC,
           wf_var_context VC ->
           check_type VC Nat Nat
| ctMatrix : forall m n VC,
           wf_var_context VC ->
           check_type VC (Matrix m n) (Matrix m n)
| ctComputation : forall P x A Q P' A' Q' VC,
           wf_var_context VC ->
           check_prop VC init_mem_context P P' ->
           check_type VC A A' ->
           check_prop ((x,A')::VC) init_mem_context Q Q' ->
           check_type VC (Computation P x A Q) (Computation P' x A' Q')

with check_prop :
     (*intput*) var_context -> heap_context -> proposition ->
     (*output*) proposition -> Prop :=
| cpHId        : forall h1 h2 h1' h2' VC HC,
                 wf_var_context VC ->
                 check_heap VC HC h1 h1' ->
                 check_heap VC HC h2 h2' ->
                 check_prop VC HC (HId h1 h2) (HId h1' h2')
| cpId         : forall A M N A' M' N' VC HC,
                 wf_var_context VC ->
                 check_type VC A A' ->
                 check_intro_term VC M A' M' ->
                 check_intro_term VC N A' N' ->
                 check_prop VC HC (Id A M N) (Id A' M' N')
| cpTop        : forall VC HC,
                 wf_var_context VC ->
                 check_prop VC HC Top Top
| cpBottom     : forall VC HC,
                 wf_var_context VC ->
                 check_prop VC HC Bottom Bottom
| cpAnd        : forall P Q P' Q' VC HC,
                 wf_var_context VC ->
                 check_prop VC HC P P' ->
                 check_prop VC HC Q Q' ->
                 check_prop VC HC (And P Q) (And P' Q')
| cpOr         : forall P Q P' Q' VC HC,
                 wf_var_context VC ->
                 check_prop VC HC P P' ->
                 check_prop VC HC Q Q' ->
                 check_prop VC HC (Or P Q) (Or P' Q')
| cpImplies    : forall P Q P' Q' VC HC,
                 wf_var_context VC ->
                 check_prop VC HC P P' ->
                 check_prop VC HC Q Q' ->
                 check_prop VC HC (Implies P Q) (Implies P' Q')
| cpNot        : forall P P' VC HC,
                 wf_var_context VC ->
                 check_prop VC HC P P' ->
                 check_prop VC HC (Not P) (Not P')
| cpIndom      : forall H H' M M' VC HC,
                 wf_var_context VC ->
                 check_intro_term VC M Nat M' ->
                 check_heap VC HC H H' ->
                 check_prop VC HC (Indom H M) (Indom H' M')
| cpForAll     : forall A P A' P' x VC HC,
                 wf_var_context VC ->
                 check_type VC A A' ->
                 check_prop ((x,A')::VC) HC P P' ->
                 check_prop VC HC (ForAll x A P) (ForAll x A' P')
| cpExists     : forall A P A' P' x VC HC,
                 wf_var_context VC ->
                 check_type VC A A' ->
                 check_prop ((x,A')::VC) HC P P' ->
                 check_prop VC HC (Exists x A P) (Exists x A' P')
| cpForAllHeap : forall P P' x VC HC,
                 wf_var_context VC ->
                 check_prop VC (x::HC) P P' ->
                 check_prop VC HC (ForAllHeap x P) (ForAllHeap x P')
| cpExistsHeap : forall P P' x VC HC,
                 wf_var_context VC ->
                 check_prop VC (x::HC) P P' ->
                 check_prop VC HC (ExistsHeap x P) (ExistsHeap x P')

with check_heap :
     (*input*) var_context -> heap_context -> heap ->
     (*output*) heap -> Prop :=
| chVar     : forall x VC HC,
              wf_var_context VC ->
              In x HC -> (*x is in the heap context*)
              check_heap VC HC (HVar x) (HVar x)
| chHEmpty  : forall VC HC,
              wf_var_context VC ->
              check_heap VC HC HEmpty HEmpty
| chHUpdate : forall A A' h h' M M' N N' VC HC,
              wf_var_context VC ->
              check_type VC A A' ->
              check_heap VC HC h h' ->
              check_intro_term VC M Nat M' ->
              check_intro_term VC N A' N' ->
              check_heap VC HC (HUpdate h M N A) (HUpdate h' M' N' A')

with check_intro_term :
     (*input*) var_context -> intro_term -> (*canonical*) type ->
     (*output*) intro_term -> Prop :=
| ciUnit     : forall VC,
               wf_var_context VC ->
               check_intro_term VC TT Unit TT
| ciBoolean  : forall VC b,
               wf_var_context VC ->
               check_intro_term VC (Boolean b) Bool (Boolean b)
| ciRef      : forall VC n,
               wf_var_context VC ->
               check_intro_term VC (Ref n) Nat (Ref n)
| ciMat      : forall m n (N : numMatrix m n) VC,
               wf_var_context VC ->
               check_intro_term VC (Mat N) (Matrix m n) (Mat N)
| ciTranspose: forall m n M M' VC,
               wf_var_context VC ->
               check_intro_term VC M (Matrix m n) M' ->
               check_intro_term VC (Unop Transpose M) (Matrix n m) (Unop Transpose M')
| ciInverse  : forall n M M' VC,
               wf_var_context VC ->
               check_intro_term VC M (Matrix n n) M' ->
               check_intro_term VC (Unop Inverse M) (Matrix n n) (Unop Inverse M')
| cibNot     : forall M M' VC,
               wf_var_context VC ->
               check_intro_term VC M Bool M' ->
               check_intro_term VC (Unop BNot M) Bool (Unop BNot M')
| ciNeg      : forall m n M M' VC,
               wf_var_context VC ->
               check_intro_term VC M (Matrix m n) M' ->
               check_intro_term VC (Unop Neg M) (Matrix m n) (Unop Neg M')
| ciMultiply : forall m n p M N M' N' VC,
               wf_var_context VC ->
               check_intro_term VC M (Matrix m n) M' ->
               check_intro_term VC N (Matrix n p) N' ->
               check_intro_term VC (Binop Multiply M N) (Matrix m p) (Binop Multiply M' N')
| ciNumBinop : forall (b : num_binop) m n M N M' N' VC,
               wf_var_context VC ->
               check_intro_term VC M (Matrix m n) M' ->
               check_intro_term VC N (Matrix m n) N' ->
               check_intro_term VC (Binop b M N) (Matrix m n) (Binop b M' N')
| ciNatBinop : forall (b : num_binop) M N M' N' VC,
               b <> Divide ->
               wf_var_context VC ->
               check_intro_term VC M Nat M' ->
               check_intro_term VC N Nat N' ->
               check_intro_term VC (Binop b M N) Nat (Binop b M' N')
| ciCompBinop: forall (b : comp_binop) m n M N M' N' VC,
               wf_var_context VC ->
               check_intro_term VC M (Matrix m n) M' ->
               check_intro_term VC N (Matrix m n) N' ->
               check_intro_term VC (Binop b M N) Bool (Binop b M' N')
| ciCompBinopBool : forall (b : comp_binop) M N M' N' VC,
               wf_var_context VC ->
               check_intro_term VC M Bool M' ->
               check_intro_term VC N Bool N' ->
               check_intro_term VC (Binop b M N) Bool (Binop b M' N')
| ciElimTerm : forall K M' A B N' VC,
               wf_var_context VC ->
               check_type VC B B (* B must be canonical *) ->
               infer_elim_term VC K A M' ->
               A = B (* A must be syntactically equal to B *) ->
               aux_expand_fun A M' = N' ->
               check_intro_term VC K B N'
| ciDia      : forall E E' P x A Q VC,
               wf_var_context VC ->
               check_postcondition VC (And (HId init mem) P) E x A Q E' ->
               check_intro_term VC (Dia E) (Computation P x A Q) (Dia E')
| ciSelectNum: forall m n M N M' N' VC,
               wf_var_context VC ->
               check_intro_term VC M (Matrix m n) M' ->
               check_intro_term VC N Nat N' ->
               check_intro_term VC (Select M N) Nat (Select M' N')

with infer_elim_term :
     (*input*) var_context -> elim_term ->
     (*output*) type -> intro_term -> Prop :=
| ieVar   : forall x A VC (pf : in_var_context x VC),
            wf_var_context VC ->
            get x VC pf = A ->
            (*check_type VC A A -> A is canonical because A is in
              the well-founded var_context VC*)
            infer_elim_term VC (Var x) A (Var x)
| ieCast  : forall M M' A A' VC,
            wf_var_context VC ->
            check_type VC A A' ->
            check_intro_term VC M A' M' ->
            infer_elim_term VC (Cast M A) A' M'

with infer_postcondition :
     (*input*) var_context -> proposition -> computation -> var -> type ->
     (*output*) proposition -> computation -> Prop :=
| ipIntroTerm : forall P M M' x A Q VC,
                wf_var_context VC ->
                check_type VC A A -> (*A is canonical*)
                check_prop VC init_mem_context P P -> (*P is canonical*)
                check_intro_term VC M A M' ->
                Q = And P (Id A (aux_expand_fun A (Var x)) M') ->
                infer_postcondition VC P M x A Q M'
| ipLetDia    : forall P x K N' E E' y (z:heap_var) B A Q R1 R2 O VC,
                wf_var_context VC ->
                check_type VC A A -> (*A is canonical*)
                check_type VC B B -> (*B is canonical*)
                check_prop VC init_mem_context P P -> (*P is canonical*)
                check_prop ((x,A)::VC) init_mem_context Q Q -> (*Q x is canonical*)
                infer_elim_term VC K (Computation R1 x A R2) N' ->
                sequent VC init_mem_context P R1 -> (*P==>R1*)
                infer_postcondition ((x,A)::VC) (seq_prop P R2 z) E y B Q E' ->
                aux_reduce A N' x E' O ->
                infer_postcondition VC P (Let dia x <- K in E) y B (Exists x A Q) O
| ipAnnotation: forall VC P (I:proposition) E y B Q I' E' z,
                wf_var_context VC ->
                check_type VC B B -> (*B is canonical*)
                check_prop VC init_mem_context P P -> (*P is canonical*)
                check_prop VC init_mem_context I I' ->
                sequent VC init_mem_context P I' ->
                infer_postcondition VC (seq_prop P I' z) E y B Q E' ->
                infer_postcondition VC P (Annotation I;; E) y B Q (Annotation I';; E')
| ipAlloc     : forall P x A A' M M' E E' y (z:heap_var) B Q sp_alloc VC,
                wf_var_context VC ->
                check_type VC B B -> (*B is canonical*)
                check_prop VC init_mem_context P P -> (*P is canonical*)
                check_type VC A A' ->
                check_intro_term VC M A' M' ->
                sp (Alloc x M' A') sp_alloc -> (*strongest postcondition for command*)
                infer_postcondition ((x,Nat)::VC) (seq_prop P sp_alloc z) E y B Q E' ->
                infer_postcondition VC P (Alloc x M A;; E) y B (Exists x Nat Q) (Alloc x M' A';; E')
| ipDealloc   : forall P x M M' A A' E E' y z B Q sp_dealloc VC,
                wf_var_context VC ->
                check_type VC B B -> (*B is canonical*)
                check_prop VC init_mem_context P P -> (*P is canonical*)
                check_type VC A A' ->
                check_intro_term VC M A' M' ->
                sequent VC init_mem_context (prop_subst "mem" init P) (seleq_ A' init M' z x) (*P==>init is defined on M'*) ->
                sp (Dealloc x M' A') sp_dealloc ->
                infer_postcondition ((x,A')::VC) (seq_prop P sp_dealloc z) E y B Q E' ->
                infer_postcondition VC P (Dealloc x M A;; E) y B (Exists z A' Q) (Dealloc x M' A';; E')
| ipLookup    : forall P x M M' A A' E E' y z B Q sp_lookup VC h,
                wf_var_context VC ->
                check_type VC B B -> (*B is canonical*)
                check_prop VC init_mem_context P P -> (*P is canonical*)
                check_type VC A A' ->
                check_intro_term VC M Nat M' ->
                sequent VC init_mem_context P (seleq_ A' mem M' h x) -> (*P==>mem is defined on M'*)
                sp (Lookup x M' A') sp_lookup -> (*strongest postcondition for command*)
                infer_postcondition ((x,A')::VC) (seq_prop P sp_lookup h) E y B Q E' ->
                infer_postcondition VC P (Lookup x M A;; E) y B (Exists z A' Q) (Lookup x M' A';; E')
| ipMutate    : forall P x M M' A A' N N' E E' y z B Q sp_mutate VC,
                wf_var_context VC ->
                check_type VC B B -> (*B is canonical*)
                check_prop VC init_mem_context P P -> (*P is canonical*)
                check_type VC A A' ->
                check_intro_term VC M Nat M' ->
                check_intro_term VC N A' N' ->
                sequent VC init_mem_context P (seleq_ A' mem M' z x) -> (*P==>mem is defined on M'*)
                sp (Mutate M' N' A') sp_mutate ->
                infer_postcondition VC (seq_prop P sp_mutate z) E y B Q E' ->
                infer_postcondition VC P (Mutate M N A;; E) y B Q (Mutate M' N' A';; E')
| ipSend      : forall VC P A M N E y B Q A' M' N' E',
                wf_var_context VC ->
                check_type VC B B -> (*B is canonical*)
                check_prop VC init_mem_context P P -> (*P is canonical*)
                check_type VC A A' ->
                check_intro_term VC M A' M'->
                check_intro_term VC N Nat N' ->
                infer_postcondition VC P E y B Q E' ->
                infer_postcondition VC P (Send A M N ;; E) y B Q (Send A' M' N' ;; E')
| ipReceive   : forall VC P x A N E y B Q A' N' E',
                wf_var_context VC ->
                check_type VC B B -> (*B is canonical*)
                check_prop VC init_mem_context P P -> (*P is canonical*)
                check_type VC A A' ->
                check_intro_term VC N Nat N' ->
                infer_postcondition ((x,A')::VC) P E y B Q E' ->
                infer_postcondition VC P (Receive x A N ;; E) y B (Exists x A' Q) (Receive x A' N' ;; E')

| ipIf        : forall P x A A' M M' E1 E1' E2 E2' E E' y B Q P1 P2 VC,
                wf_var_context VC ->
                check_type VC B B -> (*B is canonical*)
                check_prop VC init_mem_context P P -> (*P is canonical*)
                check_type VC A A' ->
                check_intro_term VC M Bool M' ->
                (*if M'==true then E1=>E1'*)
                infer_postcondition VC (And P (Id Bool M' (Boolean true))) E1 x A' P1 E1' ->
                (*if M'==false then E2=>E2'*)
                infer_postcondition VC (And P (Id Bool M' (Boolean false))) E2 x A' P2 E2' ->
                infer_postcondition ((x,A')::VC) (Or P1 P2) E y B Q E' ->
                infer_postcondition VC P (If x M A E1 E2;; E) y B (Exists x A' Q) (If x M' A' E1' E2';; E')
| ipLoop      : forall P y I I' I''' I'''' J J1 J2 J3 J4 M M' A A' x N N' N'' F F' E E' z C Q VC,
                wf_var_context VC ->
                wf_var_context ((x,A')::(y,A')::VC) ->
                wf_var_context ((x,A')::(y,A')::(z,A')::VC) ->
(*                ~ in_var_context x VC ->
                ~ in_var_context y VC ->
                ~ in_var_context z VC ->*)
                check_type VC C C -> (*C is canonical*)
                check_prop VC init_mem_context P P -> (*P is canonical*)
                check_type VC A A' ->
                check_intro_term VC M A' M' ->
                check_intro_term ((x,A')::VC) N Bool N' ->
                check_prop ((x,A')::(y,A')::VC) init_mem_context I I' -> (*get canonical loop invariant*)
                (**)
                let I'' := prop_subst "init" mem I' in
                    proposition_hereditary_subst M' y (getShape A') I'' I''' ->
                    proposition_hereditary_subst M' x (getShape A') I''' I'''' ->
                (*I holds before and after every iteration*)
                sequent VC init_mem_context P I'''' ->
                (**)
                  proposition_hereditary_subst (Var z) x (getShape A') I' J1 ->
                  proposition_hereditary_subst (Var z) y (getShape A') I' J2 ->
                (*If I holds before iteration i and between iterations i & i+1 then it holds after iteration i+1*)
                sequent ((x,A')::(y,A')::(z,A')::VC) init_mem_context (seq_prop J1 J2 z) I' ->
                (**)
                  proposition_hereditary_subst (Var y) x (getShape A') (prop_subst "init" mem I') J ->
                (*I' holds if the loop is not taken*)
                sequent ((x,A')::(y,A')::VC) init_mem_context I' J ->
                (**)
                  proposition_hereditary_subst (Var x) y (getShape A') I' J3 ->
                (*Execute the body of the loop if the loop guard is satisfied*)
                check_postcondition ((x,A')::VC)
                  (And (And (HId init mem) J3) (Id Bool N' (Boolean true)))
                  F y A' I' F' ->
                (**)
                  proposition_hereditary_subst M' x (getShape A') I' J4 ->
                  intro_term_hereditary_subst (Var y) x (getShape Bool) N' N'' ->
                (*Execute the continuation of the loop is the loop guard is not satisfied*)
                infer_postcondition ((y,A')::VC) (seq_prop P (And J4 (Id Bool N'' (Boolean false))) z)
                  E z C Q E' ->
                infer_postcondition VC P (Loop y I M A x N x F;; E) z C (Exists y A' Q)
                                         (Loop y I' M' A' x N' x F';; E')
| ipStrengthenPre : forall VC (P P':proposition) E x A Q E',
                    infer_postcondition VC P E x A Q E' ->
                    sequent VC init_mem_context P' P ->
                    infer_postcondition VC P' E x A Q E'

with check_postcondition :
     (*input*) var_context -> proposition -> computation -> var -> type -> proposition ->
     (*output*) computation -> Prop :=
| cpConsequent : forall P Q R E E' x A VC,
                 wf_var_context VC ->
                 check_type VC A A -> (* A is canonical *)
                 check_prop VC init_mem_context P P -> (*P is canonical*)
                 check_prop ((x,A)::VC) init_mem_context Q Q -> (*Q is canonical*)
                 infer_postcondition VC P E x A R E' -> (*R is the strongest postcondition*)
                 sequent ((x,A)::VC) init_mem_context R Q -> (*R ==> Q*)
                 check_postcondition VC P E x A Q E'

with sequent :
     (*input*) var_context -> heap_context -> prop_context ->
     (*output*) prop_context -> Prop :=
| sEq           : forall P PC1 PC2 VC HC,
                  wf_var_context VC ->
                  wf_prop_context VC HC PC1 ->
                  wf_prop_context VC HC PC2 ->
                  sequent VC HC (P::PC1) (P::PC2)
| sCut          : forall P PC1 PC2 VC HC,
                  wf_var_context VC ->
                  wf_prop_context VC HC PC1 ->
                  wf_prop_context VC HC PC2 ->
                  sequent VC HC PC1 (P::PC2) ->
                  sequent VC HC (P::PC1) PC2 ->
                  sequent VC HC PC1 PC2
| sSwap1        : forall VC HC P1 P2 PC1 PC2,
                  sequent VC HC (P1::P2::PC1) PC2 ->
                  sequent VC HC (P2::P1::PC1) PC2
| sSwap2        : forall VC HC P1 P2 PC1 PC2,
                  sequent VC HC PC1 (P1::P2::PC2) ->
                  sequent VC HC PC1 (P2::P1::PC2)
| sWeak1        : forall P PC1 PC2 VC HC,
                  wf_var_context VC ->
                  wf_prop_context VC HC PC1 ->
                  wf_prop_context VC HC PC2 ->
                  sequent VC HC PC1 PC2 ->
                  sequent VC HC (P::PC1) PC2
| sWeak2        : forall P PC1 PC2 VC HC,
                  wf_var_context VC ->
                  wf_prop_context VC HC PC1 ->
                  wf_prop_context VC HC PC2 ->
                  sequent VC HC PC1 PC2 ->
                  sequent VC HC PC1 (P::PC2)
| sContraction1 : forall P PC1 PC2 VC HC,  wf_var_context VC ->
                  wf_prop_context VC HC PC1 ->
                  wf_prop_context VC HC PC2 ->
                  sequent VC HC (P::P::PC1) PC2 ->
                  sequent VC HC (P::PC1) PC2
| sContraction2 : forall P PC1 PC2 VC HC,
                  wf_var_context VC ->
                  wf_prop_context VC HC PC1 ->
                  wf_prop_context VC HC PC2 ->
                  sequent VC HC PC1 (P::P::PC2) ->
                  sequent VC HC PC1 (P::PC2)

| sBottom   : forall PC1 PC2 VC HC,
              wf_var_context VC ->
              wf_prop_context VC HC PC1 ->
              wf_prop_context VC HC PC2 ->
              sequent VC HC (Bottom::PC1) PC2
| sTop      : forall PC1 PC2 VC HC,
              wf_var_context VC ->
              wf_prop_context VC HC PC1 ->
              wf_prop_context VC HC PC2 ->
              sequent VC HC PC1 (Top::PC2)
| sAnd1     : forall P Q PC1 PC2 VC HC,
              wf_var_context VC ->
              wf_prop_context VC HC PC1 ->
              wf_prop_context VC HC PC2 ->
              sequent VC HC (P::Q::PC1) PC2 ->
              sequent VC HC (And P Q::PC1) PC2
| sAnd2     : forall P Q PC1 PC2 VC HC,
              wf_var_context VC ->
              wf_prop_context VC HC PC1 ->
              wf_prop_context VC HC PC2 ->
              sequent VC HC PC1 (P::PC2) ->
              sequent VC HC PC1 (Q::PC2) ->
              sequent VC HC PC1 (And P Q::PC2)
| sOr1      : forall P Q PC1 PC2 VC HC,
              wf_var_context VC ->
              wf_prop_context VC HC PC1 ->
              wf_prop_context VC HC PC2 ->
              sequent VC HC (P::PC1) PC2 ->
              sequent VC HC (Q::PC1) PC2 ->
              sequent VC HC (Or P Q::PC1) PC2
| sOr2      : forall P Q PC1 PC2 VC HC,
              wf_var_context VC ->
              wf_prop_context VC HC PC1 ->
              wf_prop_context VC HC PC2 ->
              sequent VC HC PC1 (P::Q::PC2) ->
              sequent VC HC PC1 (Or P Q::PC2)
| sImplies1 : forall P Q PC1 PC2 VC HC,
              wf_var_context VC ->
              wf_prop_context VC HC PC1 ->
              wf_prop_context VC HC PC2 ->
              sequent VC HC PC1 (P::PC2) ->
              sequent VC HC (Q::PC1) PC2 ->
              sequent VC HC (Implies P Q::PC1) PC2
| sImplies2 : forall P Q PC1 PC2 VC HC,
              wf_var_context VC ->
              wf_prop_context VC HC PC1 ->
              wf_prop_context VC HC PC2 ->
              sequent VC HC (P::PC1) (Q::PC2) ->
              sequent VC HC PC1 (Implies P Q::PC2)
| sNot1     : forall P PC1 PC2 VC HC,
              wf_var_context VC ->
              wf_prop_context VC HC PC1 ->
              wf_prop_context VC HC PC2 ->
              sequent VC HC PC1 (P::PC2) ->
              sequent VC HC (Not P::PC1) PC2
| sNot2     : forall P PC1 PC2 VC HC,
              wf_var_context VC ->
              wf_prop_context VC HC PC1 ->
              wf_prop_context VC HC PC2 ->
              sequent VC HC (P::PC1) PC2 ->
              sequent VC HC PC1 (Not P::PC2)

| sForAllElim      : forall x A P P' M PC1 PC2 VC HC,
                     wf_var_context VC ->
                     wf_prop_context VC HC PC1 ->
                     wf_prop_context VC HC PC2 ->
                     check_intro_term VC M A M (* M is any canonical intro term *) ->
                     proposition_hereditary_subst M x (getShape A) P P' ->
                     sequent VC HC (P'::ForAll x A P::PC1) PC2 ->
                     sequent VC HC (ForAll x A P::PC1) PC2
| sForAllIntro     : forall x A P PC1 PC2 VC HC,
                     wf_var_context VC ->
                     wf_prop_context VC HC PC1 ->
                     wf_prop_context VC HC PC2 ->
                     check_type VC A A ->
                     sequent ((x,A)::VC) HC PC1 (P::PC2) ->
                     sequent VC HC PC1 (ForAll x A P::PC2)
| sExistsElim      : forall x A P PC1 PC2 VC HC,
                     wf_var_context VC ->
                     wf_prop_context VC HC PC1 ->
                     wf_prop_context VC HC PC2 ->
                     check_type VC A A ->
                     sequent ((x,A)::VC) HC (P::PC1) PC2 ->
                     sequent VC HC (Exists x A P::PC1) PC2
| sExistsIntro     : forall x A P P' M PC1 PC2 VC HC,
                     wf_var_context VC ->
                     wf_prop_context VC HC PC1 ->
                     wf_prop_context VC HC PC2 ->
                     check_intro_term VC M A M (* M is any canonical intro term *) ->
                     proposition_hereditary_subst M x (getShape A) P P' ->
                     sequent VC HC PC1 (P'::Exists x A P::PC2) ->
                     sequent VC HC PC1 (Exists x A P::PC2)
| sForAllHeapElim  : forall x h P PC1 PC2 VC HC,
                     wf_var_context VC ->
                     wf_prop_context VC HC PC1 ->
                     wf_prop_context VC HC PC2 ->
                     check_heap VC HC h h (* h is any canonical heap *) ->
                     sequent VC HC (prop_subst x h P::ForAllHeap x P::PC1) PC2 ->
                     sequent VC HC (ForAllHeap x P::PC1) PC2
| sForAllHeapIntro : forall x P PC1 PC2 VC HC,
                     wf_var_context VC ->
                     wf_prop_context VC HC PC1 ->
                     wf_prop_context VC HC PC2 ->
                     sequent VC (x::HC) PC1 (P::PC2) ->
                     sequent VC HC PC1 (ForAllHeap x P::PC2)
| sExistsHeapElim : forall x P PC1 PC2 VC HC,
                     wf_var_context VC ->
                     wf_prop_context VC HC PC1 ->
                     wf_prop_context VC HC PC2 ->
                     sequent VC (x::HC) (P::PC1) PC2 ->
                     sequent VC HC (ExistsHeap x P::PC1) PC2
| sExistsHeapIntro : forall h x P PC1 PC2 VC HC,
                     wf_var_context VC ->
                     wf_prop_context VC HC PC1 ->
                     wf_prop_context VC HC PC2 ->
                     check_heap VC HC h h (* h is any canonical heap *) ->
                     sequent VC HC PC1 (prop_subst x h P::ExistsHeap x P::PC2) ->
                     sequent VC HC PC1 (ExistsHeap x P::PC2)

(* type equality *)
| sIdEq     : forall A M PC1 PC2 VC HC,
              wf_var_context VC ->
              wf_prop_context VC HC PC1 ->
              wf_prop_context VC HC PC2 ->
              sequent VC HC PC1 (Id A M M::PC2)
| sIdSubst1 : forall A M N x Q Q1 Q2 PC1 PC2 VC HC,
              wf_var_context VC ->
              wf_prop_context VC HC PC1 ->
              wf_prop_context VC HC PC2 ->
              proposition_hereditary_subst N x (getShape A) Q Q1 ->
              proposition_hereditary_subst M x (getShape A) Q Q2 ->
              sequent VC HC (Id A M N::PC1) (Q1::PC2) ->
              sequent VC HC (Id A M N::PC1) (Q2::PC2)
| sIdSubst2 : forall A M N x Q Q1 Q2 PC1 PC2 VC HC,
              wf_var_context VC ->
              wf_prop_context VC HC PC1 ->
              wf_prop_context VC HC PC2 ->
              proposition_hereditary_subst N x (getShape A) Q Q1 ->
              proposition_hereditary_subst M x (getShape A) Q Q2 ->
              sequent VC HC (Id A M N::PC1) (Q2::PC2) ->
              sequent VC HC (Id A M N::PC1) (Q1::PC2)

(* heaps *)
| sHIdEq           : forall H PC1 PC2 VC HC,
                     wf_var_context VC ->
                     wf_prop_context VC HC PC1 ->
                     wf_prop_context VC HC PC2 ->
                     sequent VC HC PC1 (HId H H::PC2)
| sHIdSubst1       : forall H1 H2 h q q1' q2' PC1 PC2 VC HC,
                     wf_var_context VC ->
                     wf_prop_context VC HC PC1 ->
                     wf_prop_context VC HC PC2 ->
                     prop_subst h H1 q = q1' ->
                     prop_subst h H2 q = q2' ->
                     sequent VC HC (HId H1 H2::PC1) (q1'::PC2) ->
                     sequent VC HC (HId H1 H2::PC1) (q2'::PC2)
| sHIdSubst2       : forall H1 H2 h q q1' q2' PC1 PC2 VC HC,
                     wf_var_context VC ->
                     wf_prop_context VC HC PC1 ->
                     wf_prop_context VC HC PC2 ->
                     prop_subst h H1 q = q1' ->
                     prop_subst h H2 q = q2' ->
                     sequent VC HC (HId H1 H2::PC1) (q2'::PC2) ->
                     sequent VC HC (HId H1 H2::PC1) (q1'::PC2)
| sHIdSubstIntro1  : forall H1 H2 h q q1' q2' PC1 PC2 VC HC,
                     wf_var_context VC ->
                     wf_prop_context VC HC PC1 ->
                     wf_prop_context VC HC PC2 ->
                     prop_subst h H1 q = q1' ->
                     prop_subst h H2 q = q2' ->
                     sequent VC HC (HId H1 H2::q1'::PC1) PC2 ->
                     sequent VC HC (HId H1 H2::q2'::PC1) PC2
| sHIdPermutation  : forall M1 N1 M2 N2 A B H PC1 PC2 VC HC,
                     wf_var_context VC ->
                     wf_prop_context VC HC PC1 ->
                     wf_prop_context VC HC PC2 ->
                     sequent VC HC PC1 (Id Nat M1 M2::HId (HUpdate (HUpdate H M1 N1 B) M2 N2 A)
                                                          (HUpdate (HUpdate H M2 N2 A) M1 N1 B)::PC2)
| sHIdUpdateCancel : forall H M N1 N2 A B PC1 PC2 VC HC,
                     wf_var_context VC ->
                     wf_prop_context VC HC PC1 ->
                     wf_prop_context VC HC PC2 ->
                     sequent VC HC PC1 (HId (HUpdate (HUpdate H M N1 B) M N2 A)
                                            (HUpdate H M N2 A)::PC2)
| sFunctionalHeap  : forall H1 H2 M N1 N2 A PC1 PC2 VC HC,
                     wf_var_context VC ->
                     wf_prop_context VC HC PC1 ->
                     wf_prop_context VC HC PC2 ->
                     sequent VC HC (HId (HUpdate H1 M N1 A) (HUpdate H2 M N2 A)::PC1)
                                   (Id A N1 N2::PC2)
| sEmptyHeap       : forall H M N A PC1 PC2 VC HC,
                     wf_var_context VC ->
                     wf_prop_context VC HC PC1 ->
                     wf_prop_context VC HC PC2 ->
                     sequent VC HC (HId HEmpty (HUpdate H M N A)::PC1) PC2
| sInDom           : forall H1 H2 M N A PC1 PC2 VC HC,
                     wf_var_context VC ->
                     wf_prop_context VC HC PC1 ->
                     wf_prop_context VC HC PC2 ->
                     sequent VC HC (HId H1 (HUpdate H2 M N A)::PC1) (Indom H1 M::PC2)

(*other*)
| sId            : forall A M N PC1 PC2 VC HC,
                   wf_var_context VC ->
                   wf_prop_context VC HC PC1 ->
                   wf_prop_context VC HC PC2 ->
                   normalize M = normalize N ->
                   sequent VC HC PC1 (Id A M N::PC2)
.

Scheme mut_wf_var_context := Induction for wf_var_context Sort Prop
with mut_wf_prop_contrext := Induction for wf_prop_context Sort Prop
with mut_check_type := Induction for check_type Sort Prop
with mut_check_prop := Induction for check_prop Sort Prop
with mut_check_heap := Induction for check_heap Sort Prop
with mut_check_intro_term := Induction for check_intro_term Sort Prop
with mut_infer_elim_term := Induction for infer_elim_term Sort Prop
with mut_infer_postcondition := Induction for infer_postcondition Sort Prop
with mut_check_postcondition := Induction for check_postcondition Sort Prop
with mut_sequent := Induction for sequent Sort Prop.

End typing.
Hint Constructors check_type check_prop check_heap check_intro_term infer_elim_term wf_var_context wf_prop_context.

author: jpaykin

repo: ControlHTT

save_path: github-repos/coq/jpaykin-ControlHTT


text:
(* Base Helix defintions: data types, utility functions, lemmas *)

Global Generalizable All Variables.

Require Import Coq.Arith.Arith.
Require Import Coq.Arith.Minus.
Require Import Coq.Arith.EqNat.
Require Import Coq.Arith.Lt.
Require Import Coq.Program.Program.
Require Import Coq.Classes.Morphisms.
Require Import Coq.Strings.String.
Require Import Coq.Logic.Decidable.
Require Export Coq.Init.Specif.

Require Import Helix.Tactics.HelixTactics.

Require Import Psatz.
Require Import Coq.micromega.Lia.

Require Import Coq.Logic.FunctionalExtensionality.
Require Import MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders.
Require Import MathClasses.orders.minmax MathClasses.orders.orders MathClasses.orders.rings.
Require Import MathClasses.theory.abs.
Require Import MathClasses.theory.setoids.

Require Import CoLoR.Util.Nat.NatUtil.

Definition string_beq a b := if string_dec a b then true else false.

Global Instance max_proper A `{Le A, TotalOrder A, !Setoid A}
       `{!∀ x y: A, Decision (x ≤ y)}:
  Proper ((=) ==> (=) ==> (=)) max.
Proof.
  solve_proper.
Qed.

Global Instance negate_proper A `{Ar: Ring A} `{!Setoid A}:
  Setoid_Morphism (negate).
Proof.
  split;try assumption.
  solve_proper.
Qed.

Lemma ne_sym {T:Type} `{E: Equiv T} `{S: @Setoid T E} {a b: T}:
  (a ≠ b) <-> (b ≠ a).
Proof.
  crush.
Qed.

Global Instance abs_Setoid_Morphism A
         `{Ar: Ring A}
         `{Asetoid: !Setoid A}
         `{Ato: !@TotalOrder A Ae Ale}
         `{Aabs: !@Abs A Ae Ale Azero Anegate}
  : Setoid_Morphism abs | 0.
Proof.
  split; try assumption.
  intros x y E.
  unfold abs, abs_sig.
  destruct (Aabs x) as [z1 [Ez1 Fz1]]. destruct (Aabs y) as [z2 [Ez2 Fz2]].
  simpl.
  rewrite <-E in Ez2, Fz2.
  destruct (total (≤) 0 x).
  now rewrite Ez1, Ez2.
  now rewrite Fz1, Fz2.
Qed.

Lemma abs_nonneg_s `{Aabs: Abs A}: forall (x : A), 0 ≤ x → abs x = x.
Proof.
  intros AA AE. unfold abs, abs_sig.
  destruct (Aabs AA).  destruct a.
  auto.
Qed.

Lemma abs_nonpos_s `{Aabs: Abs A} (x : A): x ≤ 0 → abs x = -x.
Proof.
  intros E. unfold abs, abs_sig. destruct (Aabs x) as [z1 [Ez1 Fz1]]. auto.
Qed.

Lemma abs_0_s
      `{Ae: Equiv A}
      `{Ato: !@TotalOrder A Ae Ale}
      `{Aabs: !@Abs A Ae Ale Azero Anegate}
  : abs 0 = 0.
Proof.
  apply abs_nonneg_s. auto.
Qed.

Lemma abs_always_nonneg
      `{Ae: Equiv A}
      `{Az: Zero A} `{A1: One A}
      `{Aplus: Plus A} `{Amult: Mult A}
      `{Aneg: Negate A}
      `{Ale: Le A}
      `{Ato: !@TotalOrder A Ae Ale}
      `{Aabs: !@Abs A Ae Ale Az Aneg}
      `{Ar: !Ring A}
      `{ASRO: !@SemiRingOrder A Ae Aplus Amult Az A1 Ale}
  : forall x, 0 ≤ abs x.
Proof.
  intros.
  destruct (total (≤) 0 x).
  rewrite abs_nonneg_s; assumption.
  rewrite abs_nonpos_s.
  rewrite <- flip_nonpos_negate; assumption.
  assumption.
Qed.

Lemma abs_negate_s A (x:A)
      `{Ae: Equiv A}
      `{Az: Zero A} `{A1: One A}
      `{Aplus: Plus A} `{Amult: Mult A}
      `{Aneg: Negate A}
      `{Ale: Le A}
      `{Ato: !@TotalOrder A Ae Ale}
      `{Aabs: !@Abs A Ae Ale Az Aneg}
      `{Ar: !Ring A}
      `{ASRO: !@SemiRingOrder A Ae Aplus Amult Az A1 Ale}
  : abs (-x) = abs x.
Proof with trivial.
  destruct (total (≤) 0 x).
  -
    rewrite (abs_nonneg x), abs_nonpos.
    apply rings.negate_involutive.
    apply flip_nonneg_negate.
    apply H.
    apply H.
  -
    rewrite (abs_nonneg (-x)), abs_nonpos.
    reflexivity.
    apply H.
    apply flip_nonpos_negate.
    apply H.
Qed.

Lemma abs_nz_nz
      `{Ae: Equiv A}
      `{Az: Zero A} `{A1: One A}
      `{Aplus: Plus A} `{Amult: Mult A}
      `{Aneg: Negate A}
      `{Ale: Le A}
      `{Ato: !@TotalOrder A Ae Ale}
      `{Aabs: !@Abs A Ae Ale Az Aneg}
      `{Ar: !Ring A}
      `{Aledec: ∀ x y: A, Decision (x ≤ y)}
  :
    forall v : A, v ≠ zero <-> abs v ≠ zero.
Proof.
  split.
  -
    intros V.
    destruct (Aledec zero v).
    +
      apply abs_nonneg_s in l.
      rewrite l.
      apply V.
    +
      apply orders.le_flip in n.
      rewrite abs_nonpos_s; auto.
      apply rings.flip_negate_ne_0, V.
  -
    intros V.
    destruct (Aledec zero v) as [E | N].
    +
      apply abs_nonneg_s in E.
      rewrite <- E.
      apply V.
    +
      apply orders.le_flip in N.
      apply abs_nonpos_s in N.
      apply rings.flip_negate_ne_0.
      rewrite <- N.
      apply V.
Qed.

Global Instance abs_idempotent
         `{Ae: Equiv A}
         `{Az: Zero A} `{A1: One A}
         `{Aplus: Plus A} `{Amult: Mult A}
         `{Aneg: Negate A}
         `{Ale: Le A}
         `{Ato: !@TotalOrder A Ae Ale}
         `{Aabs: !@Abs A Ae Ale Az Aneg}
         `{Ar: !Ring A}
         `{ASRO: !@SemiRingOrder A Ae Aplus Amult Az A1 Ale}
  :UnaryIdempotent abs.
Proof.
  intros a b E.
  unfold compose.
  destruct (total (≤) 0 a).
  rewrite abs_nonneg_s.
  auto.
  apply abs_always_nonneg.
  setoid_replace (abs a) with (-a) by apply abs_nonpos_s.
  rewrite abs_negate_s.
  auto.
  apply Ato.
  apply Ar.
  apply ASRO.
  apply H.
Qed.

Local Open Scope nat_scope.

Lemma modulo_smaller_than_devisor:
  ∀ x y : nat, 0 ≢ y → x mod y < y.
Proof.
  intros.
  destruct y; try congruence.
  unfold PeanoNat.Nat.modulo.
  lia.
Qed.

Lemma ext_equiv_applied_equiv
      `{Equiv A} `{Equiv B}
      `(!Setoid_Morphism (f : A → B))
      `(!Setoid_Morphism (g : A → B)) :
  f = g ↔ ∀ x, f x = g x.
Proof.
  pose proof (setoidmor_a f).
  pose proof (setoidmor_b f).
  split; intros E1.
  now apply ext_equiv_applied.
  intros x y E2. now rewrite E2.
Qed.

Lemma zero_lt_Sn:
  forall n:nat, 0<S n.
Proof.
  intros.
  lia.
Qed.

Lemma S_j_lt_n {n j:nat}:
  S j ≡ n -> j < n.
Proof.
  intros H.
  rewrite <- H.
  auto.
Qed.

Lemma Decidable_decision
      (P:Prop):
  Decision P -> decidable P.
Proof.
  intros D.
  unfold decidable.
  destruct D; tauto.
Qed.

Lemma div_iff_0:
  forall m i : nat, m ≢ 0 → i/m≡0 -> m>i.
Proof.
  intros m i M H.
  destruct (Compare_dec.dec_lt i m) as [HL|HGE].
  -
    lia.
  -
    apply Nat.nlt_ge in HGE.
    destruct (eq_nat_dec i m).
    *
      subst i.
      rewrite Nat.div_same in H.
      congruence.
      apply M.
    *
      assert(G:i>m) by crush.
      apply NatUtil.gt_plus in G.
      destruct G.
      rename x into k.
      subst i.
      replace (k + 1 + m) with (1*m+(k+1)) in H by ring.
      rewrite Nat.div_add_l in H.
      simpl in H.
      congruence.
      apply M.
Qed.

Lemma div_ne_0:
  ∀ m i : nat, m <= i → m ≢ 0 → i / m ≢ 0.
Proof.
  intros m i H MZ.
  unfold not.
  intros M.
  apply div_iff_0 in M.
  destruct M; crush.
  apply MZ.
Qed.

Lemma add_lt_lt
     {n m t : nat}:
  (t < m) ->  (t + n < n + m).
Proof.
  lia.
Qed.

(* Similar to `Vnth_cast_aux` but arguments in equality hypotheis are swapped *)
Lemma eq_lt_lt {n m k: nat} : n ≡ m -> k < n -> k < m.
Proof. intros; lia. Qed.

Lemma S_pred_simpl:
  forall n : nat, n ≢ 0 -> S (Init.Nat.pred n) ≡ n.
Proof.
  intros n H.
  destruct n.
  - congruence.
  - auto.
Qed.

Global Instance Sig_Equiv {A:Type} {Ae : Equiv A} {P:A->Prop}:
  Equiv (@sig A P) := fun a b => (proj1_sig a) = (proj1_sig b).

Instance proj1_proper {A:Type} {Ae : Equiv A} {P:A->Prop}:
  Proper ((=)==>(=)) (@proj1_sig A P).
Proof.
  intros x y E.
  unfold equiv, Sig_Equiv in E.
  auto.
Qed.

Require Import MathClasses.implementations.peano_naturals.

Ltac nat_equiv_to_eq :=
  match goal with
  | [H: @equiv nat peano_naturals.nat_equiv ?a ?b |- _] => unfold equiv, peano_naturals.nat_equiv in H
  end.

Require Import Coq.Strings.String.

(* Maybe later move to separate .v file *)
Section StringUtils.

  Open Scope nat_scope.
  Open Scope string_scope.

  (* Lifted from Software foundations *)
  Fixpoint string_of_nat_aux (time n : nat) (acc : string) : string :=
    let d := match Nat.modulo n 10 with
             | 0 => "0" | 1 => "1" | 2 => "2" | 3 => "3" | 4 => "4" | 5 => "5"
             | 6 => "6" | 7 => "7" | 8 => "8" | _ => "9"
             end in
    let acc' := append d acc in
    match time with
    | 0 => acc'
    | S time' =>
      match Nat.div n 10 with
      | 0 => acc'
      | n' => string_of_nat_aux time' n' acc'
      end
    end.

  Definition string_of_nat (n : nat) : string :=
    string_of_nat_aux n n "".

End StringUtils.

Definition is_Some_bool {A:Type} (x:option A) : bool :=
  match x with
  | Some x => true
  | None => false
  end.

Definition is_None_bool {A:Type} (x:option A) : bool :=
  match x with
  | Some x => false
  | None => true
  end.

author: asosyuk


text:
(* -*- mode: coq; mode: visual-line -*-  *)

From HoTT Require Import Basics.
From WildCat Require Export Cat1.

(** * The unit category *)

CoFixpoint isglob_unit : IsGlob 0 Unit
  := Build_IsGlob 0 Unit (fun _ _ => Unit) (fun _ _ => isglob_unit).

Global Existing Instance isglob_unit.

CoFixpoint iscat0_unit : IsCat0 0 Unit.
Proof.
  snrapply Build_IsCat0.
  1,2,5: intros; exact tt.
  (** We cannot use isfunctor0_const since that requires IsCat0 *)
  1,2:
    intros ? ? ? ?; cofix e;
    simple notypeclasses refine (Build_IsFunctor0 _ _ _);
    intros ? ?; [ intro; exact tt | exact e ].
  intros a b.
  apply iscat0_unit.
Defined.

Global Existing Instance iscat0_unit.

author: Alizter

repo: WildCat

save_path: github-repos/coq/Alizter-WildCat


text:
Fixpoint le_f (n m : nat) {struct n} : Prop :=
  match n with
    | O => True
    | S n' =>
      match m with
	| O => False
	| S m' => le_f n' m'
      end
  end.

Theorem le_f_transitive : forall n1 n2 n3,
  le_f n1 n2
  -> le_f n2 n3
  -> le_f n1 n3.
  induction n1; simpl; intuition.

  destruct n2; intuition.
  simpl in H0.
  destruct n3; intuition.
  apply IHn1 with n2; assumption.
Qed.

Inductive le : nat -> nat -> Prop :=
  | le_n : forall n, le n n
  | le_S : forall n m, le n m -> le n (S m).

Theorem le_transitive : forall n1 n2 n3,
  le n1 n2
  -> le n2 n3
  -> le n1 n3.
  induction 2; intros.

  assumption.

  apply le_S.
  apply IHle.
  assumption.
Qed.

Check le_ind.

Theorem le_transitive_easy : forall n1 n2 n3,
  n1 <= n2
  -> n2 <= n3
  -> n1 <= n3.
  induction 2; intuition.
Qed.

Lemma le_O' : forall n m, n <= m -> m = 0 -> n = 0.
  destruct 1.

  trivial.

  intro.
  discriminate.
Qed.

Theorem le_O : forall n, n <= 0 -> n = 0.
  intros.
  apply le_O' with 0.
  assumption.
  reflexivity.
Qed.

Theorem le_O_easy : forall n, n <= 0 -> n = 0.
  inversion 1; reflexivity.
Qed.

(** * Sorted lists *)

Require Import List.

Inductive sorted : list nat -> Prop :=
  | sorted_nil :
    sorted nil
  | sorted_one : forall n,
    sorted (n :: nil)
  | sorted_cons : forall n m ls,
    n <= m
    -> sorted (m :: ls)
    -> sorted (n :: m :: ls).

Theorem sorted_123 : sorted (1 :: 2 :: 3 :: nil).
  apply sorted_cons.
  auto.
  apply sorted_cons.
  auto.
  apply sorted_one.
Qed.

Theorem sorted_123_easy : sorted (1 :: 2 :: 3 :: nil).
  Hint Constructors sorted.
  auto.
Qed.

Inductive sublist : list nat -> list nat -> Prop :=
  | sub_nil :
    sublist nil nil
  | sub_keep : forall x ls ls',
    sublist ls ls'
    -> sublist (x :: ls) (x :: ls')
  | sub_drop : forall x ls ls',
    sublist ls ls'
    -> sublist (x :: ls) ls'.

Theorem sublist_1234_23 : sublist (1 :: 2 :: 3 :: 4 :: nil) (2 :: 3 :: nil).
  apply sub_drop.
  apply sub_keep.
  apply sub_keep.
  apply sub_drop.
  apply sub_nil.
Qed.

Theorem sublist_1234_23_easy : sublist (1 :: 2 :: 3 :: 4 :: nil) (2 :: 3 :: nil).
  Hint Constructors sublist.
  auto.
Qed.

Lemma sorted_sublist' : forall ls ls',
  sublist ls ls'
  -> sorted ls
  -> match ls, ls' with
       | x :: _, y :: _ => x <= y
       | _, _ => True
     end.
  induction 1; intuition.

  inversion H0; subst.

  inversion H.
  trivial.

  intuition.
  destruct ls'.
  trivial.
  apply le_transitive_easy with m; assumption.
Qed.

Theorem sorted_sublist : forall ls,
  sorted ls
  -> forall ls', sublist ls ls'
    -> sorted ls'.
  induction 1; intuition.

  inversion H.
  apply sorted_nil.

  inversion H; subst.
  inversion H3; subst.
  apply sorted_one.

  inversion H3; subst.
  apply sorted_nil.

  inversion H1; subst.
  destruct ls'0.

  apply sorted_one.

  apply sorted_cons.

  apply le_transitive_easy with m.
  assumption.
  apply (sorted_sublist' (m :: ls) (n0 :: ls'0)).
  assumption.
  assumption.

  apply IHsorted.
  assumption.

  apply IHsorted.
  assumption.
Qed.

(** * An interpreter *)

Definition var := nat.

Inductive exp : Set :=
  | Num : nat -> exp
  | Bool : bool -> exp

  | Var : var -> exp

  | Plus : exp -> exp -> exp
  | Eq : exp -> exp -> exp.

Require Import Arith.
Definition env := var -> exp.

Inductive isValue : exp -> Prop :=
  | ValueNum : forall n, isValue (Num n)
  | ValueBool : forall n, isValue (Bool n).

Inductive eval (G : env) : exp -> exp -> Prop :=
  | EvalValue : forall e, isValue e -> eval G e e
  | EvalVar : forall x, eval G (Var x) (G x)
  | EvalPlus : forall e1 e2 n1 n2,
    eval G e1 (Num n1)
    -> eval G e2 (Num n2)
    -> eval G (Plus e1 e2) (Num (n1 + n2))
  | EvalEq_True : forall e1 e2 n,
    eval G e1 (Num n)
    -> eval G e2 (Num n)
    -> eval G (Eq e1 e2) (Bool true)
  | EvalEq_False : forall e1 e2 n1 n2,
    eval G e1 (Num n1)
    -> eval G e2 (Num n2)
    -> n1 <> n2
    -> eval G (Eq e1 e2) (Bool false).

Inductive type : Set :=
  | TyNum : type
  | TyBool : type.

Section typing.
  Variable Gtypes : var -> type.
  Variable G : env.

  Inductive hasType : exp -> type -> Prop :=
    | HT_Num : forall n,
      hasType (Num n) TyNum
    | HT_Bool : forall b,
      hasType (Bool b) TyBool

    | HT_Var : forall x,
      hasType (Var x) (Gtypes x)

    | HT_Plus : forall e1 e2,
      hasType e1 TyNum
      -> hasType e2 TyNum
      -> hasType (Plus e1 e2) TyNum
    | HT_Eq : forall e1 e2,
      hasType e1 TyNum
      -> hasType e2 TyNum
      -> hasType (Eq e1 e2) TyBool.

  Definition Gtyped :=
    (forall x, isValue (G x))
    /\ (forall x,
      hasType (G x) (Gtypes x)).

  Hypothesis G_typed : Gtyped.

  Theorem eval_is_safe : forall e t,
    hasType e t
    -> exists v, eval G e v
      /\ isValue v
      /\ hasType v t.
    unfold Gtyped in G_typed.
    induction 1.

    exists (Num n).
    intuition.
    apply EvalValue.
    apply ValueNum.
    apply ValueNum.
    apply HT_Num.

    exists (Bool b).
    intuition.
    apply EvalValue.
    apply ValueBool.
    apply ValueBool.
    apply HT_Bool.

    exists (G x).
    intuition.
    apply EvalVar.

    firstorder.
    destruct H4.
    destruct H7.
    exists (Num (n + n0)).
    intuition.
    apply EvalPlus; assumption.
    apply ValueNum.
    apply HT_Num.

    inversion H8.
    inversion H5.

    firstorder.
    destruct H4.
    destruct H7.
    destruct (eq_nat_dec n n0).

    subst.
    exists (Bool true).
    intuition.
    apply EvalEq_True with n0; assumption.
    apply ValueBool.
    apply HT_Bool.

    exists (Bool false).
    intuition.
    apply EvalEq_False with n n0; assumption.
    apply ValueBool.
    apply HT_Bool.

    inversion H8.
    inversion H5.
  Qed.

  Hint Constructors isValue eval hasType.

  Lemma eval_Num : forall v,
    isValue v
    -> hasType v TyNum
    -> exists n, v = Num n.
    destruct 1.
    eauto.
    inversion 1.
  Qed.

  Theorem eval_is_safe_easier : forall e t,
    hasType e t
    -> exists v, eval G e v
      /\ isValue v
      /\ hasType v t.
    red in G_typed.
    induction 1; firstorder; eauto.

    generalize (eval_Num x H4 H5).
    generalize (eval_Num x0 H7 H8).
    firstorder; subst; eauto.

    generalize (eval_Num x H4 H5).
    generalize (eval_Num x0 H7 H8).
    firstorder; subst.
    destruct (eq_nat_dec x2 x1); subst; eauto.
  Qed.
End typing.

Inductive cmd : Set :=
  | Skip : cmd
  | Write : var -> exp -> cmd
  | Seq : cmd -> cmd -> cmd
  | If : exp -> cmd -> cmd -> cmd.

Definition bind (G : env) (x : var) (e : exp) :=
  fun (x' : var) =>
    if eq_nat_dec x x'
      then e
      else G x'.

Inductive exec : env -> cmd -> env -> Prop :=
  | ExecSkip : forall G, exec G Skip G

  | ExecWrite : forall G x e v,
    eval G e v
    -> exec G (Write x e) (bind G x v)

  | ExecSeq : forall G c1 c2 G' G'',
    exec G c1 G'
    -> exec G' c2 G''
    -> exec G (Seq c1 c2) G''

  | ExecIf_True : forall G e c1 c2 G',
    eval G e (Bool true)
    -> exec G c1 G'
    -> exec G (If e c1 c2) G'

  | ExecIf_False : forall G e c1 c2 G',
    eval G e (Bool false)
    -> exec G c2 G'
    -> exec G (If e c1 c2) G'.

Section cmd_typing.
  Variable Gtypes : var -> type.

  Inductive valid : cmd -> Prop :=
    | ValidSkip :
      valid Skip

    | ValidWrite : forall x e,
      hasType Gtypes e (Gtypes x)
      -> valid (Write x e)

    | ValidSeq : forall c1 c2,
      valid c1
      -> valid c2
      -> valid (Seq c1 c2)

    | ValidIf : forall e c1 c2,
      hasType Gtypes e TyBool
      -> valid c1
      -> valid c2
      -> valid (If e c1 c2).

  Hint Constructors exec valid.

  Hint Unfold Gtyped.

  Lemma eval_Bool : forall v,
    isValue v
    -> hasType Gtypes v TyBool
    -> exists b, v = Bool b.
    destruct 1.
    inversion 1.
    eauto.
  Qed.

  Theorem exec_is_safe: forall c,
    valid c
    -> forall G, Gtyped Gtypes G
      -> exists G', exec G c G'
	/\ Gtyped Gtypes G'.
    induction 1; intros.

    exists G; intuition.

    destruct (eval_is_safe Gtypes G H0 e (Gtypes x) H); intuition.
    exists (bind G x x0); intuition.
    red in H0.
    split; intros; unfold bind;
      destruct (eq_nat_dec x x1); subst; intuition.

    destruct (IHvalid1 _ H1); intuition.
    destruct (IHvalid2 _ H4); intuition.
    eauto.

    destruct (eval_is_safe Gtypes G H2 e TyBool H); intuition.
    destruct (eval_Bool x H3 H6); subst.
    destruct x0.

    destruct (IHvalid1 _ H2); intuition; eauto.
    destruct (IHvalid2 _ H2); intuition; eauto.
  Qed.

End cmd_typing.

author: SatyendraBanjare

repo: itp

save_path: github-repos/coq/SatyendraBanjare-itp


text:
(* *********************************************************************)
(*                                                                     *)
(*            The CertiKOS Certified Kit Operating System              *)
(*                                                                     *)
(*                   The FLINT Group, Yale University                  *)
(*                                                                     *)
(*  Copyright The FLINT Group, Yale University.  All rights reserved.  *)
(*  This file is distributed under the terms of the Yale University    *)
(*  Non-Commercial License Agreement.                                  *)
(*                                                                     *)
(* *********************************************************************)
(* *********************************************************************)
(*                                                                     *)
(*       Lemmas about the Clight used in various C level proofs        *)
(*                                                                     *)
(*                 Developed by Xiongnan (Newman) Wu                   *)
(*                                                                     *)
(*                         Yale University                             *)
(*                                                                     *)
(* *********************************************************************)

Require Import Coqlib.
Require Import Maps.
Require Import Integers.
Require Import Values.
Require Import Memory.
Require Import EventsX.
Require Import Clight.
Require Import Cop.
Require Import Ctypes.
Require Import ZArith.

 Hint Unfold Int.max_unsigned.
 Hint Unfold Int.modulus.
 Hint Unfold Int.half_modulus.
 Hint Unfold Int64.max_unsigned.
 Hint Unfold Int64.modulus.
 Hint Unfold Int64.half_modulus.

 Open Scope Z_scope.

 (** * Frequently used lemmas in tactics. *)

 Lemma zadd_rm_head: forall n p q, p = q -> n + p = n + q.
 Proof.
   intros.
   rewrite H.
   trivial.
 Qed.

 Lemma zadd_rm_tail: forall n p q, p = q -> p + n = q + n.
 Proof.
   intros.
   rewrite H.
   trivial.
 Qed.

 Lemma zdiv_range_le_lt : forall a b c x: Z, a <= 0 -> b > 0 -> c > 0 -> a <= x < b -> a <= x/ c < b.
 Proof.
   intros.
   destruct H2.
   split.
   apply Zdiv_le_lower_bound.
   omega.
   assert(a * c <= a).
   assert(- a * c >= - a).
   rewrite <- Zmult_1_r.
   assert(c >= 1) by omega.
   apply Zmult_ge_compat_l.
   omega.
   omega.
   rewrite Zopp_mult_distr_l_reverse in H4.
   omega.
   omega.
   apply Zdiv_lt_upper_bound.
   omega.
   assert(b <= b * c).
   rewrite <- Zmult_1_r at 1.
   assert(1 <= c) by omega.
   apply Zmult_le_compat_l.
   omega.
   omega.
   omega.
 Qed.

 Lemma zdiv_range_le_le : forall a b c x: Z, a <= 0 -> b > 0 -> c > 0 -> a <= x <= b -> a <= x/ c <= b.
 Proof.
   intros.
   destruct H2.
   split.
   apply Zdiv_le_lower_bound.
   omega.
   assert(a * c <= a).
   assert(- a * c >= - a).
   rewrite <- Zmult_1_r.
   assert(c >= 1) by omega.
   apply Zmult_ge_compat_l.
   omega.
   omega.
   rewrite Zopp_mult_distr_l_reverse in H4.
   omega.
   omega.
   apply Zdiv_le_upper_bound.
   omega.
   assert(b <= b * c).
   rewrite <- Zmult_1_r at 1.
   assert(1 <= c) by omega.
   apply Zmult_le_compat_l.
   omega.
   omega.
   omega.
 Qed.

 Lemma max_unsigned_gt0: Int.max_unsigned > 0.
 Proof.
   repeat autounfold.
   simpl.
   omega.
 Qed.

 Lemma max_unsigned_val: Int.max_unsigned  = 4294967295.
 Proof.
   repeat autounfold; reflexivity.
 Qed.

 Lemma unsigned_inj : forall a b, Int.unsigned a = Int.unsigned b -> a = b.
 Proof.
   intros. rewrite <- (Int.repr_unsigned a).
   rewrite <- (Int.repr_unsigned b).
   f_equal.
   trivial.
 Qed.

 Lemma max_unsigned64_gt0: Int64.max_unsigned > 0.
 Proof.
   repeat autounfold.
   simpl.
   omega.
 Qed.

 Lemma max_unsigned64_val: Int64.max_unsigned  = 18446744073709551615.
 Proof.
   repeat autounfold; reflexivity.
 Qed.

 Lemma unsigned64_inj : forall a b, Int64.unsigned a = Int64.unsigned b -> a = b.
 Proof.
   intros. rewrite <- (Int64.repr_unsigned a).
   rewrite <- (Int64.repr_unsigned b).
   f_equal.
   trivial.
 Qed.

 Lemma minus1lt: forall i:Z, i - 1 < i.
 Proof.
   intro.
   omega.
 Qed.

 Lemma Z_land_range_lo: forall x y, 0 <= x -> 0 <= Z.land x y.
 Proof.
   intros.
   rewrite Z.land_nonneg.
   left.
   assumption.
 Qed.

 Lemma Z_land_range_lo_r: forall x y, 0 <= y -> 0 <= Z.land x y.
 Proof.
   intros.
   rewrite Z.land_nonneg.
   right.
   assumption.
 Qed.

 Lemma Z_land_range_hi: forall x y, 0 <= x <= Int.max_unsigned -> 0 <= y <= Int.max_unsigned -> Z.land x y <= Int.max_unsigned.
 Proof.
   rewrite max_unsigned_val.
   intros.
   assert(Z.land x y < 4294967296).
     apply Z.log2_lt_cancel.
     assert(Z.log2 (Z.land x y) <= Z.min (Z.log2 x) (Z.log2 y)).
       apply Z.log2_land.
       omega.
       omega.
     rewrite Zmin_spec in H1.
     destruct (zlt (Z.log2 x) (Z.log2 y)).
     assert(Z.log2 x <= Z.log2 4294967295).
       apply Z.log2_le_mono.
       omega.
     simpl in *.
     omega.
     assert(Z.log2 y <= Z.log2 4294967295).
       apply Z.log2_le_mono.
       omega.
     simpl in *.
     omega.
   omega.
 Qed.

 Lemma Z_land_range: forall x y, 0 <= x <= Int.max_unsigned -> 0 <= y <= Int.max_unsigned -> 0 <= Z.land x y <= Int.max_unsigned.
 Proof.
   split.
   apply Z_land_range_lo; omega.
   apply Z_land_range_hi; omega.
 Qed.

 Lemma Z64_land_range_hi: forall x y, 0 <= x <= Int64.max_unsigned -> 0 <= y <= Int64.max_unsigned -> Z.land x y <= Int64.max_unsigned.
 Proof.
   rewrite max_unsigned64_val.
   intros.
   assert (Z.land x y < 18446744073709551616).
     apply Z.log2_lt_cancel.
     assert(Z.log2 (Z.land x y) <= Z.min (Z.log2 x) (Z.log2 y)).
       apply Z.log2_land.
       omega.
       omega.
     rewrite Zmin_spec in H1.
     destruct (zlt (Z.log2 x) (Z.log2 y)).
     assert(Z.log2 x <= Z.log2 18446744073709551615).
       apply Z.log2_le_mono.
       omega.
     simpl in *.
     omega.
     assert(Z.log2 y <= Z.log2 18446744073709551615).
       apply Z.log2_le_mono.
       omega.
     simpl in *.
     omega.
   omega.
 Qed.

 Lemma Z64_land_range: forall x y, 0 <= x <= Int64.max_unsigned -> 0 <= y <= Int64.max_unsigned -> 0 <= Z.land x y <= Int64.max_unsigned.
 Proof.
   split.
   apply Z_land_range_lo; omega.
   apply Z64_land_range_hi; omega.
 Qed.

 Lemma Z_lor_range_lo: forall x y, 0 <= x -> 0 <= y -> 0 <= Z.lor x y.
 Proof.
   intros.
   apply Z.lor_nonneg; auto.
 Qed.

 Lemma Z_lor_range_hi: forall x y, 0 <= x <= Int.max_unsigned -> 0 <= y <= Int.max_unsigned -> Z.lor x y <= Int.max_unsigned.
 Proof.
   rewrite max_unsigned_val; simpl.
   intros.
   assert(Z.lor x y < 4294967296).
     apply Z.log2_lt_cancel.
     assert(Z.log2 (Z.lor x y) = Z.max (Z.log2 x) (Z.log2 y)).
       apply Z.log2_lor.
       omega.
       omega.
     rewrite H1.
     rewrite Zmax_spec in *.
     destruct (zlt (Z.log2 y) (Z.log2 x)).
     assert(Z.log2 x <= Z.log2 4294967295).
       apply Z.log2_le_mono.
       omega.
     simpl in *.
     omega.
     assert(Z.log2 y <= Z.log2 4294967295).
       apply Z.log2_le_mono.
       omega.
     simpl in *.
     omega.
   omega.
 Qed.

 Lemma Z_lor_range: forall x y, 0 <= x <= Int.max_unsigned -> 0 <= y <= Int.max_unsigned -> 0 <= Z.lor x y <= Int.max_unsigned.
 Proof.
   intros.
   split.
   apply Z_lor_range_lo; omega.
   apply Z_lor_range_hi; omega.
 Qed.

 Lemma Z64_lor_range_hi: forall x y, 0 <= x <= Int64.max_unsigned -> 0 <= y <= Int64.max_unsigned -> Z.lor x y <= Int64.max_unsigned.
 Proof.
   rewrite max_unsigned64_val; simpl.
   intros.
   assert(Z.lor x y < 18446744073709551616).
     apply Z.log2_lt_cancel.
     assert(Z.log2 (Z.lor x y) = Z.max (Z.log2 x) (Z.log2 y)).
       apply Z.log2_lor.
       omega.
       omega.
     rewrite H1.
     rewrite Zmax_spec in *.
     destruct (zlt (Z.log2 y) (Z.log2 x)).
     assert(Z.log2 x <= Z.log2 18446744073709551615).
       apply Z.log2_le_mono.
       omega.
     simpl in *.
     omega.
     assert(Z.log2 y <= Z.log2 18446744073709551615).
       apply Z.log2_le_mono.
       omega.
     simpl in *.
     omega.
   omega.
 Qed.

 Lemma Z64_lor_range: forall x y, 0 <= x <= Int64.max_unsigned -> 0 <= y <= Int64.max_unsigned -> 0 <= Z.lor x y <= Int64.max_unsigned.
 Proof.
   split.
   apply Z_lor_range_lo; omega.
   apply Z64_lor_range_hi; omega.
 Qed.

 Lemma Z_lxor_range :
   forall x y,
     0 <= x <= Int.max_unsigned -> 0 <= y <= Int.max_unsigned ->
     0 <= Z.lxor x y <= Int.max_unsigned.
 Proof.
   rewrite max_unsigned_val; simpl.
   intros.
   split.
   rewrite Z.lxor_nonneg.
   split; omega.
   assert(Z.lxor x y < 4294967296).
     apply Z.log2_lt_cancel.
     assert(Z.log2 (Z.lxor x y) <= Z.max (Z.log2 x) (Z.log2 y)).
       apply Z.log2_lxor.
       omega.
       omega.
     apply Z.le_lt_trans with (m := Z.max (Z.log2 x) (Z.log2 y)); auto.
     rewrite Zmax_spec in *.
     destruct (zlt (Z.log2 y) (Z.log2 x)).
     assert(Z.log2 x <= Z.log2 4294967295).
       apply Z.log2_le_mono.
       omega.
     simpl in *.
     omega.
     assert(Z.log2 y <= Z.log2 4294967295).
       apply Z.log2_le_mono.
       omega.
     simpl in *.
     omega.
   omega.
 Qed.

 Lemma Z_shiftl_16_range :
   forall x,
     0 <= x < 65536 -> 0 <= Z.shiftl x 16 <= Int.max_unsigned.
 Proof.
   unfold Int.max_unsigned. simpl (Int.modulus - 1).
   intros.
   split.
   rewrite Z.shiftl_nonneg. omega.

   assert (Z.shiftl x 16 < 4294967296).
     case_eq (zeq x 0); intros; subst.

     (* x = 0 *)
     simpl. omega.

     (* x <> 0 *)
     apply Z.log2_lt_cancel.
     rewrite Z.log2_shiftl; try omega.

     assert (Z.log2 x <= Z.log2 65535).
       apply Z.log2_le_mono. omega.
     simpl in *. omega.

   omega.
 Qed.

 Lemma Z_shiftl_32_range :
   forall x,
     0 <= x <= Int.max_unsigned -> 0 <= Z.shiftl x 32 <= Int64.max_unsigned.
 Proof.
   unfold Int.max_unsigned, Int64.max_unsigned.
   simpl (Int.modulus - 1); simpl (Int64.modulus - 1).
   intros x H; simpl in H.
   split.
   - (*"0 <= (x << 32)"*)
     rewrite Z.shiftl_nonneg; omega.
   - (*"(x << 32) <= Int64.max_unsigned"*)
     assert (Hx32: Z.shiftl x 32 < 18446744073709551616).
     + (*"assertion"*)
       case_eq (zeq x 0); intros; subst.
       * (*"x == 0"*)
         simpl. omega.
       *  (*"x <> 0"*)
         apply Z.log2_lt_cancel.
         rewrite Z.log2_shiftl; try omega.
         assert (Z.log2 x <= Z.log2 4294967295).
         {
           (*"assertion"*)
           apply Z.log2_le_mono; omega.
         }
         simpl in *; omega.
     + omega.
 Qed.

  (** * Hints for autorewrite *)

  Lemma unsigned_zero: Int.unsigned Int.zero = 0.
  Proof. reflexivity. Qed.

  Lemma unsigned_one: Int.unsigned Int.one = 1.
  Proof. reflexivity. Qed.

  Lemma eq_one_zero: Int.eq Int.one Int.zero = false.
  Proof. reflexivity. Qed.

  Lemma eq_zero_zero: Int.eq Int.zero Int.zero = true.
  Proof. reflexivity. Qed.

  Lemma negb_true: negb true = false.
  Proof. reflexivity. Qed.

  Lemma negb_false: negb false = true.
  Proof. reflexivity. Qed.

  Lemma repr_zero: Int.repr 0 = Int.zero.
  Proof. reflexivity. Qed.

  Lemma repr_one: Int.repr 1 = Int.one.
  Proof. reflexivity. Qed.

  Lemma and_zero_zero: Z.land 0 0 = 0.
  Proof. reflexivity. Qed.

  Lemma and_one_zero: Z.land 1 0 = 0.
  Proof. reflexivity. Qed.

  Lemma and_zero_one: Z.land 0 1 = 0.
  Proof. reflexivity. Qed.

  Lemma and_one_one: Z.land 1 1 = 1.
  Proof. reflexivity. Qed.

  Lemma or_zero_zero: Z.lor 0 0 = 0.
  Proof. reflexivity. Qed.

  Lemma or_one_zero: Z.lor 1 0 = 1.
  Proof. reflexivity. Qed.

  Lemma or_zero_one: Z.lor 0 1 = 1.
  Proof. reflexivity. Qed.

  Lemma or_one_one: Z.lor 1 1 = 1.
  Proof. reflexivity. Qed.

  Hint Rewrite unsigned_zero unsigned_one eq_one_zero eq_zero_zero negb_true negb_false repr_zero repr_one: arith.
  Hint Rewrite and_zero_zero and_zero_one and_one_zero and_one_one or_zero_zero or_zero_one or_one_zero or_one_one : arith.

  Lemma list_disjoint_nil: forall (A: Type) (l1: list A), list_disjoint l1 nil.
  Proof.
    intros.
    unfold list_disjoint.
    simpl.
    intros.
    contradiction.
  Qed.

  (** * Common useful tactics *)

  Ltac Caseeq H := generalize H; apply or_ind; clear H.

  Require String. Open Scope string_scope.

  Ltac move_to_top x :=
    match reverse goal with
      | H : _ |- _ => try move x after H
    end.

  Tactic Notation "assert_eq" ident(x) constr(v) :=
    let H := fresh in
    assert (x = v) as H by reflexivity;
      clear H.

  Tactic Notation "Case_aux" ident(x) constr(name) :=
    first [
        set (x := name); move_to_top x
      | assert_eq x name; move_to_top x
      | fail 1 "because we are working on a different case" ].

  Tactic Notation "Case" constr(name) := Case_aux Case name.
  Tactic Notation "SCase" constr(name) := Case_aux SCase name.
  Tactic Notation "SSCase" constr(name) := Case_aux SSCase name.
  Tactic Notation "SSSCase" constr(name) := Case_aux SSSCase name.
  Tactic Notation "SSSSCase" constr(name) := Case_aux SSSSCase name.
  Tactic Notation "SSSSSCase" constr(name) := Case_aux SSSSSCase name.
  Tactic Notation "SSSSSSCase" constr(name) := Case_aux SSSSSSCase name.
  Tactic Notation "SSSSSSSCase" constr(name) := Case_aux SSSSSSSCase name.

repo: certikos


text:
(******************************************************************
  Definitions of general tree and BST, where BST is constructed as
  a tree with the proof that it's BST.
  Functions such as insert, search, and equivalences between tree
  and list of elements from in-order tree traversal.
  Various lemmas, theorems that prove properties of the functions.

  Author: :p
  *****************************************************************)

Require Import EqNat.
Require Import PeanoNat.
Require Import String.
Require Import BinNums.
Require Import List.
Require Import Compare_dec.
Require Import Omega.
Set Implicit Arguments.

Section TREE.

(** Type for the keys of the tree.
  Could potentially be polymorphic, with requirements of decidable equality and total ordering. *)
Definition K: Type := nat.

Variable V: Type.

Inductive Tree : Type :=
  | null : Tree
  | node : K->V->Tree->Tree->Tree.

Theorem is_null_dec: forall t, {t = null} + {t <> null}.
Proof.
induction t; simpl; intros.
left. reflexivity.
right. intro. discriminate.
Qed.

(* general predicate *)
Fixpoint tree_all_keys (t: Tree) (p: K->V->Prop) : Prop :=
  match t with
  | null => True
  | node k v lt rt  => p k v /\ (tree_all_keys lt p) /\ (tree_all_keys rt p)
  end.

Definition tree_min (t: Tree) (k: K): Prop :=
  tree_all_keys t (fun k' _  => k' > k).

Definition tree_max (t: Tree) (k: K): Prop :=
  tree_all_keys t (fun k' _ => k' < k).

Fixpoint is_bst (t: Tree) : Prop :=
  match t with
  | null            => True
  | node k v lt rt  => (tree_max lt k) /\ (tree_min rt k) /\ (is_bst lt) /\ (is_bst rt)
  end.

(* binary search tree *)
Inductive BST : Type :=
  | tree : forall t, is_bst t -> BST.

Lemma null_bst_proof : is_bst null.
Proof.
repeat constructor. Qed.

Definition null_BST : BST :=
  tree (null) null_bst_proof.

Check null_BST.

Fixpoint tree_insert (tr: Tree) (a: K) (v: V) : Tree :=
  match tr with
  | null                => node a v null null
  | node key val ltr rtr    => if a =? key then node key v ltr rtr
                           else (if a <? key then node key val (tree_insert ltr a v) rtr
                                 else node key val ltr (tree_insert rtr a v))
  end.

Lemma all_after_insert: forall t a v p, tree_all_keys t p -> p a v -> tree_all_keys (tree_insert t a v) p.
Proof.
induction t; simpl; intros.
auto. remember (a =? k) as c. destruct c. constructor. symmetry in Heqc. apply Nat.eqb_eq in Heqc.
rewrite <- Heqc. apply H0. apply H.
remember (a <? k) as d. destruct d; simpl. split; try (apply H). split.
apply IHt1. apply H. apply H0. apply H.
split; try (apply H). split. apply H. apply IHt2. apply H. apply H0.
Qed.

Lemma gt_lemma: forall a k, false = (a =? k) -> false = (a <? k) -> a > k.
Proof. intros.
assert (a <> k). { intro. apply Nat.eqb_eq in H1. rewrite H1 in H. discriminate. }
apply not_eq in H1. destruct H1.
apply Nat.ltb_lt in H1. rewrite H1 in H0. discriminate.
auto.
Qed.

(** Theorem: tree_insert works, invariance.
    Crucial for the self-verifying definition of BST_insert *)
Theorem insert_proof : forall (tr: Tree) (a: K) (v: V), is_bst tr -> is_bst (tree_insert tr a v).
Proof.
intros tr a v. induction tr; simpl. easy.
intros. remember (a =? k) as d. destruct d; simpl.
  apply H. remember (a <? k) as c. destruct c.  simpl.
  split; try (apply H). destruct H.
  apply all_after_insert. apply H. symmetry in Heqc. apply Nat.ltb_lt in Heqc. apply Heqc.
  split; try (apply H). split. apply IHtr1. apply H. apply H.
  simpl. split; try (apply H). split.
  apply all_after_insert. apply H.
  apply gt_lemma; auto.
  split. apply H. apply IHtr2. apply H.
Qed.

Definition BST_insert (tr: BST) (a: K) (v: V) : BST :=
  match tr with
  | tree t proof_t  => tree (tree_insert t a v) (insert_proof t a v proof_t)
  end.

Fixpoint tree_search (tr: Tree) (k: K) : option V :=
  match tr with
  | null => None
  | node key val ltr rtr => if k =? key then Some val
                            else (if k <? key then tree_search ltr k
                                  else tree_search rtr k)
  end.

Definition bst_search (tr: BST) (k: K) : option V :=
  match tr with
  | tree t proof_t       => tree_search t k
  end.

(** Theorems for tree and BST: what is inserted is seachable. *)
Theorem insert_retrieve: forall tr k v, tree_search (tree_insert tr k v) k = Some v.
Proof.
induction tr; simpl; intros.
- (* empty initial tree *)
rewrite <- beq_nat_refl. easy.
- (* nonempty initial tree *)
remember (k0 =? k) as match_root. destruct match_root; simpl.
+ (* inserting at root *)
rewrite <- Heqmatch_root. easy.
+ (* inserting at left or right. inductive case *)
remember (k0 <? k) as lt_root.
destruct lt_root; simpl; rewrite <- Heqmatch_root; rewrite <- Heqlt_root.
apply IHtr1. apply IHtr2.
Qed.

Theorem BST_insert_retrieve : forall tr k v, bst_search (BST_insert tr k v) k = Some v.
Proof.
unfold bst_search, BST_insert. induction tr; simpl; intros. apply insert_retrieve.
Qed.

Lemma nat_not_equal: forall n m, n <> m <-> (n =? m) = false.
Proof.
intros.
destruct (Nat.eq_dec n m).
-
split. contradiction. intro not_same. apply Nat.eqb_eq in e. rewrite e in not_same. discriminate.
-
split; intro; try easy.
remember (n =? m) as same. symmetry in Heqsame. destruct same; try easy.
apply Nat.eqb_eq in Heqsame. contradiction.
Qed.

(** Theorems for tree and BST: search for a key after insersion for a different key
    is unaffected by the insersion. *)
Theorem tree_insert_skip: forall tr k1 v k2,
  k2 <> k1 -> tree_search (tree_insert tr k1 v) k2 = tree_search tr k2.
Proof.
intros. apply nat_not_equal in H.
induction tr; simpl.
- rewrite H. destruct ( k2 <? k1); reflexivity.
- remember (k1 =? k) as c_isequal. destruct c_isequal; subst.
  + remember (k2 =? k) as d_isequal. destruct d_isequal; subst.
  symmetry in Heqc_isequal. apply Nat.eqb_eq in Heqc_isequal.
  symmetry in Heqd_isequal. apply Nat.eqb_eq in Heqd_isequal.
  rewrite <- Heqd_isequal in Heqc_isequal. rewrite Heqc_isequal in H.
  apply nat_not_equal in H. omega.
  remember (k2 <? k) as c. destruct c; simpl.
  rewrite <-  Heqd_isequal.  rewrite <- Heqc. reflexivity.
  rewrite <- Heqc.  rewrite <- Heqd_isequal. reflexivity.
  + remember (k1 <? k) as d. destruct d; simpl.
  rewrite IHtr1. reflexivity. rewrite IHtr2. reflexivity.
Qed.

Theorem bst_insert_skip : forall (tr:BST) k1 v k2,
  k2 <> k1 -> bst_search (BST_insert tr k1 v) k2 = bst_search tr k2.
Proof.
intros. destruct tr. eapply tree_insert_skip in H.
simpl. apply H. Qed.

(* get all elements in the tree, in order *)
Fixpoint tree_elements (tr: Tree) : list (K * V) :=
  match tr with
  | null            => nil
  | node k v lt rt  => (tree_elements lt) ++ (cons (k, v) (tree_elements rt))
  end.

Definition bst_elements (tr: BST) : list (K * V) :=
  match tr with
  | tree t proof_t  => tree_elements t
  end.

Definition sorted_helper (a: K*V) (ls: list (K*V)) : Prop :=
  match ls with
  | nil             => True
  | cons a' ls'     => if (fst a <? fst a') then True else False
  end.

Fixpoint list_sorted (ls: list (K*V)) : Prop :=
  match ls with
  | nil           => True
  | cons a ls'    => (sorted_helper a ls') /\ list_sorted ls'
  end.

(* a bunch of useful lemmas for proving the monotonicity *)
Lemma tree_all_keys_elements: forall t k v p,
  In (k, v) (tree_elements t) -> tree_all_keys t p -> p k v.
Proof.
induction t; simpl; intros. inversion H.
apply in_app_iff in H. destruct H.
apply IHt1. apply H. apply H0.
simpl in H. destruct H. injection H; intros; subst. apply H0.
apply IHt2. apply H. apply H0.
Qed.

Lemma cons_sorted : forall rt p v,
  list_sorted (tree_elements rt)
  -> tree_min rt p -> list_sorted ((p, v) :: (tree_elements rt)).
Proof.
induction rt; simpl; try auto; intros.
split.
- inversion H0. remember (tree_elements rt1 ++ (k, v) :: tree_elements rt2) as ls.
  destruct ls. simpl. auto. simpl.
  replace (p <? fst p0) with true. constructor. symmetry. apply Nat.ltb_lt. destruct p0. simpl.
  remember (tree_elements rt1) as rt_elts. destruct rt_elts; simpl in Heqls; injection Heqls; intros; subst.
+ omega.
+ destruct H2.
assert (In (k0, v1) (tree_elements rt1)). { rewrite <- Heqrt_elts. simpl. left. reflexivity. }
eapply tree_all_keys_elements in H4; try eauto. simpl in H4. omega.
- apply H.
Qed.

Lemma cons_ls_sorted : forall a l,
  list_sorted (a :: l) -> list_sorted l.
Proof.
intros. simpl in H. destruct H. apply H0. Qed.

Lemma app_sorted: forall l rt p v,
  list_sorted l -> list_sorted (tree_elements rt) ->
  tree_min rt p -> Forall (fun e => fst e < p) l ->
  list_sorted (l ++ (p, v) :: (tree_elements rt)).
Proof.
Opaque list_sorted.
induction l; simpl; intros.
- apply cons_sorted. assumption. assumption.
- Transparent list_sorted. simpl.
split.
+ simpl in H.
destruct l. simpl. replace (fst a <? p) with true. easy. inversion H2; subst.
symmetry. apply Nat.ltb_lt. assumption.
simpl. destruct p0. destruct a. simpl.
simpl in H. apply H.
+ apply IHl. eapply cons_ls_sorted; eauto. assumption. assumption. inversion H2; subst. assumption.
Qed.

Lemma max_lt_list : forall t p x,
  tree_max t p -> In x (tree_elements t) -> fst x < p.
Proof.
intros.
destruct x. simpl. eapply tree_all_keys_elements in H. eauto . eauto.
Qed.

Lemma concat_sorted : forall lt rt p v,
  list_sorted (tree_elements lt) -> list_sorted (tree_elements rt)
  -> tree_max lt p -> tree_min rt p -> list_sorted ((tree_elements lt) ++ (p, v) :: (tree_elements rt)).
Proof.
intros.
apply app_sorted.
apply H.  apply H0. apply H2.
apply Forall_forall.
intros. eapply max_lt_list. eapply H1. apply H3.
Qed.

(** Theorems for tree and BST: monotonicity of the elements. *)
Lemma elements_tree_monotone : forall tr,
  is_bst tr -> list_sorted (tree_elements tr).
Proof.
intros tr. induction tr; simpl. auto.
intros. apply concat_sorted. apply IHtr1. apply H.
apply IHtr2. apply H. apply H.  apply H.
Qed.

Theorem elements_monotone : forall (tr: BST),
  list_sorted (bst_elements tr).
Proof.
intros. destruct tr. simpl. apply elements_tree_monotone. apply i.
Qed.

(* useful lemmas for proving the main theorems below *)
Lemma tree_found : forall tr k v,
  tree_search tr k = Some v -> In (k, v) (tree_elements tr).
Proof.
intros tr k v.
induction tr; simpl.
intro H. inversion H.
remember (k =? k0) as a eqn:Heq. destruct a.
- intro. symmetry in Heq. apply Nat.eqb_eq in Heq; subst. inversion H.
  rewrite <- H1. simpl. apply in_app_iff. right. simpl. left. reflexivity.
- remember (k <? k0) as a eqn:Hle. destruct a.
  + intro. apply IHtr1 in H. eapply in_app_iff. left. apply H.
  + intro. apply IHtr2 in H. eapply in_app_iff. right. apply in_cons. apply H.
Qed.

Lemma tree_equiv_helper : forall k v k0 v0 tr1 tr2,
  In (k, v) (tree_elements (node k0 v0 tr1 tr2)) <->
  (k, v) = (k0, v0) \/ In (k, v) (tree_elements tr1) \/ In (k, v) (tree_elements tr2).
Proof.
intros k v k0 v0 tr1 tr2. simpl. split.
- intros. apply in_app_iff in H. inversion H.
  right. left.  apply H0.
  simpl in H0. inversion H0. rewrite H1. auto. right. right. apply H1.
- intros. apply in_app_iff. inversion H. simpl. rewrite H0. auto.
  inversion H0. left. apply H1. simpl. right. right. apply H1.
Qed.

Lemma tree_equiv_helper' : forall k v k0 v0 tr1 tr2,
  tree_search (node k0 v0 tr1 tr2) k = Some v ->
  (k0, v0) = (k, v) \/ tree_search tr1 k = Some v \/ tree_search tr2 k = Some v.
Proof.
simpl.
intros.
remember (k =? k0) as a; destruct a. left. symmetry in Heqa.
apply Nat.eqb_eq in Heqa. subst.
inversion H. auto. symmetry in Heqa.
remember (k <? k0) as b. destruct b.
right. left. assumption.
right. right. assumption.
Qed.

(** Theorems for BST: the list of elements is equivalent to the tree nodes searchable
  aka. all elements got by tree traversal can be found by tree search, vice versa *)
Theorem tree_equiv : forall tr k v,
  is_bst tr -> (In (k, v) (tree_elements tr) <-> tree_search tr k = Some v).
Proof.
intros tr k v.
induction tr.
- (* null tree *)
intros. split; intros; inversion H0.
- (* real stuff!! *)
intros. split; try (apply tree_found).
intros. simpl in H.
apply tree_equiv_helper in H0.
destruct H. destruct H1. destruct H2. assert (H2' := H2). assert (H3' := H3).
apply IHtr1 in H2. apply IHtr2 in H3.
destruct H0. simpl. injection H0; intros; subst. replace (k0 =? k0) with true.
reflexivity. symmetry. apply Nat.eqb_eq. reflexivity.
destruct H0. assert (H0' := H0). simpl.  eapply tree_all_keys_elements in H0; try eauto.
simpl in H0.
replace (k =? k0) with false. apply Nat.ltb_lt in H0. rewrite H0.
apply H2. apply H0'. symmetry. apply nat_not_equal. intro. omega.
assert (H0' := H0). simpl. eapply tree_all_keys_elements in H0; try eauto.
simpl in H0.
replace (k =? k0) with false. replace (k <? k0) with false. apply H3. apply H0'.
symmetry. remember (k <? k0) as Hfal. destruct Hfal. symmetry in HeqHfal. apply Nat.ltb_lt in HeqHfal.
omega. reflexivity. symmetry. apply nat_not_equal. omega.
Qed.

Theorem bst_equiv : forall (tr:BST) k v,
  In (k, v) (bst_elements tr) <-> bst_search tr k = Some v.
Proof.
intros. destruct tr. apply tree_equiv. apply i. Qed.

(** Theorems for BST: if we can't find in search, we can't find in list, vice versa *)
Theorem element_not_found: forall (tr:BST) k,
  bst_search tr k = None <-> ~ In k (map fst (bst_elements tr)).
Proof.
intros. split.
- (* -> *)
intros. intro. apply in_map_iff in H0. destruct H0. destruct H0.
destruct x . apply bst_equiv in H1. simpl in H0. subst.
rewrite H1 in H. discriminate.
- (* <- *)
intro. unfold not in H.
assert (forall o, (forall v:V, ~ o = Some v) -> o = None).
{ intros Hv. destruct Hv. intros. assert (Some v <> Some v).
apply H0. assert (Some v = Some v). reflexivity. contradiction.
intros. reflexivity. }
apply H0 with (o:=bst_search tr k). intros. intro.
apply bst_equiv in H1. apply H. apply in_map_iff. exists (k, v).
simpl. split; try auto.
Qed.

Lemma min_no_search: forall t k, tree_min t k -> tree_search t k = None.
Proof.
intros.
remember (tree_search t k) as found.
destruct found.
symmetry in Heqfound. apply tree_found in Heqfound.
eapply tree_all_keys_elements in Heqfound; eauto.
simpl in Heqfound. omega.
easy.
Qed.

Section REMOVE.

Fixpoint tree_find_remove_max (t: Tree) : (Tree * option (K * V)) :=
  match t with
  | null => (null, None)
  | node k v ltr null => (ltr, Some (k, v))
  | node k v ltr rtr => let (rtr_removed, max) := tree_find_remove_max rtr in
      (node k v ltr rtr_removed, max)
  end.

Definition tree_remove_root (t: Tree) : Tree :=
  match t with
  | null => null
  | node k v null rtr => rtr
  | node k v ltr null => ltr
  | node k v ltr rtr => let (ltr_removed, new_root) := tree_find_remove_max ltr in
    match new_root with None => t (* impossible *)
    | Some (k', v') => node k' v' ltr_removed rtr
    end
  end.

Fixpoint tree_remove (t: Tree) (k: K) : Tree :=
  match t with
  | null => null
  | node k' v ltr rtr => if k =? k' then tree_remove_root t
                         else if k <? k' then
                         (node k' v (tree_remove ltr k) rtr) else
                         (node k' v ltr (tree_remove rtr k))
  end.

(** Theorems and lemmas which include remove *)
Lemma remove_max_satisfies_all: forall t rm_t max p
  (REM: (rm_t, max) = tree_find_remove_max t)
  (SAT: tree_all_keys t p),
  tree_all_keys rm_t p.
Proof.
induction t; simpl; intros.
injection REM; intros; subst.
simpl. constructor.
destruct t2.
injection REM; intros; subst. apply SAT.
remember (tree_find_remove_max (node k0 v0 t2_1 t2_2)) as rm_max. destruct rm_max.
injection REM; intros; subst.
simpl.
split. apply SAT.
split. apply SAT.
apply IHt2 with o. auto. apply SAT.
Qed.

Lemma tree_find_remove_max_bst : forall t rm_t max
  (ISBST: is_bst t) (REMOVE: tree_find_remove_max t = (rm_t, max)), is_bst rm_t.
Proof.
induction t; simpl; intros.
+
injection REMOVE; intros; subst. simpl. constructor.
+ (* only induct down the right *) clear IHt1.
destruct ISBST as (MAX & MIN & LEFTBST & RIGHTBST).
destruct t2.
- (* rtr is null *)
injection REMOVE; intros; subst. assumption.
- (* rtr is not null *)
remember (tree_find_remove_max (node k0 v0 t2_1 t2_2)) as removed.
destruct removed.
injection REMOVE; intros; subst.
simpl.
split. assumption.
split. eapply remove_max_satisfies_all; eauto.
split. assumption.
eapply IHt2; eauto.
Qed.

Lemma tree_all_keys_trans: forall t (p q: K->V->Prop),
  (forall k v, p k v -> q k v) ->
  tree_all_keys t p ->
  tree_all_keys t q.
Proof.
induction t; simpl; intros.
constructor.
split. apply H. apply H0.
split. eapply IHt1; eauto. apply H0. eapply IHt2; eauto. apply H0.
Qed.

Lemma tree_max_in: forall t rm_t k v
  (REMOVE: tree_find_remove_max t = (rm_t, Some (k, v))), In (k, v) (tree_elements t).
Proof.
induction t; simpl; intros.
discriminate.
destruct t2.
injection REMOVE; intros; subst.
apply in_app_iff. right. simpl. auto.
remember (tree_find_remove_max (node k1 v1 t2_1 t2_2)) as removed. destruct removed.
injection REMOVE; intros; subst.
apply in_app_iff. right. apply in_cons. eapply IHt2; eauto.
Qed.

Lemma tree_find_remove_max_max: forall t rm_t k v
  (ISBST: is_bst t) (REMOVE: tree_find_remove_max t = (rm_t, Some (k, v))), tree_max rm_t k.
Proof.
induction t; simpl; intros.
injection REMOVE; intros; subst. unfold tree_max. simpl. constructor.
destruct t2.
- (* rtr is null *)
injection REMOVE; intros; subst.
apply ISBST.
- (* rtr is not null *)
remember (tree_find_remove_max (node k1 v1 t2_1 t2_2)) as removed.
destruct removed.
destruct ISBST as (MAX & MIN & LEFTBST & RIGHTBST).
injection REMOVE; intros; subst.
assert (tree_max t k0) as MAXRM. { eapply IHt2; eauto. }
assert (k < k0) as ROOTMAX. {
symmetry in Heqremoved. apply tree_max_in in Heqremoved.
eapply tree_all_keys_elements in Heqremoved; try eapply MIN.
simpl in Heqremoved. omega.
}
split.
apply ROOTMAX.
split; try apply MAXRM.
apply tree_all_keys_trans with (p := fun (k': K) (_: V) => k' < k).
intros. omega.
apply MAX.
Qed.

Lemma tree_find_remove_max_nonempty :
  forall t, t <> null -> exists m rm_t, tree_find_remove_max t = (rm_t, Some m).
Proof.
induction t; intros.
- simpl. contradiction.
- remember t2 as t2'.
  destruct t2'.
  + simpl. eauto.
  + rewrite  Heqt2' in *.
    assert (t2 <> null). { subst t2. intro. discriminate. }
    apply IHt2 in H0. destruct H0. destruct H0. exists x.
    simpl. destruct t2; try discriminate. rewrite H0. exists (node k v t1 x0). reflexivity.
Qed.

Lemma tree_find_remove_max_empty:
  forall t rm_t, tree_find_remove_max t = (rm_t, None) -> t = null.
Proof.
intros.
destruct (is_null_dec t).
assumption.
apply tree_find_remove_max_nonempty in n.
destruct n. destruct H0. rewrite H in H0. discriminate.
Qed.

Lemma remove_root_satisfies_all: forall t p
  (SAT: tree_all_keys t p),
  tree_all_keys (tree_remove_root t) p.
Proof.
Opaque tree_find_remove_max.
destruct t; simpl; intros.
constructor.
remember t2 as t2'. remember t1 as t1'.
destruct t1'.
apply SAT.
destruct t2'.
apply SAT.
rewrite Heqt1' in *. rewrite Heqt2' in *.
remember (tree_find_remove_max t1) as removed.
destruct removed. destruct o.
-
destruct p0.
simpl.
assert (A := Heqremoved). symmetry in A.
apply tree_max_in in A. eapply tree_all_keys_elements in A; try apply SAT.
split. apply A. split. eapply remove_max_satisfies_all; eauto. apply SAT.
apply SAT.
-
symmetry in Heqremoved.
apply tree_find_remove_max_empty in Heqremoved. subst.
simpl. split. apply SAT. split. apply SAT. apply SAT.
Qed.

Lemma tree_remove_root_bst: forall t rm_t (ISBST: is_bst t) (REMOVE: tree_remove_root t = rm_t),
  is_bst rm_t.
Proof.
Opaque tree_find_remove_max.
destruct t; simpl; intros.
subst. apply null_bst_proof.
destruct t1. subst. apply ISBST.
destruct t2. subst. apply ISBST.
remember (tree_find_remove_max (node k0 v0 t1_1 t1_2)) as tree_removed.
destruct tree_removed.
 (* destructing on the tree_find_remove_max cases *)
destruct o; simpl.
- (* when o is some p *)
destruct p. subst. simpl. symmetry in Heqtree_removed.
split.  eapply tree_find_remove_max_max; try (eapply Heqtree_removed). apply ISBST.
split. assert (In (k2, v2) (tree_elements (node k0 v0 t1_1 t1_2))).
{ eapply tree_max_in; try (eapply Heqtree_removed). }
apply tree_all_keys_trans with (p := fun (k': K) (_: V) => k' > k).
intros. assert (k > k2). { eapply tree_all_keys_elements in H; try (eapply ISBST).
simpl in H. omega. } omega.
simpl. split; try (apply ISBST).
split. eapply tree_find_remove_max_bst; try (eapply Heqtree_removed). apply ISBST.
apply ISBST.
- (* when o is None *)
Transparent tree_find_remove_max.
assert ((node k0 v0 t1_1 t1_2) <> null). {intro. discriminate. }
apply tree_find_remove_max_nonempty in H. destruct H. destruct H.
rewrite <- Heqtree_removed in H. discriminate.
Qed.

Lemma remove_satisfies_all: forall t p k
  (SAT: tree_all_keys t p),
  tree_all_keys (tree_remove t k) p.
Proof.
Opaque tree_remove_root.
induction t; simpl; intros.
constructor.
destruct (k0 =? k).
apply remove_root_satisfies_all. simpl. apply SAT.
destruct (k0 <? k); simpl.
split. apply SAT. split. apply IHt1. apply SAT. apply SAT.
split. apply SAT. split. apply SAT. apply IHt2. apply SAT.
Qed.

Theorem tree_remove_bst : forall t rm_t k (ISBST: is_bst t) (REMOVE: tree_remove t k = rm_t),
  is_bst rm_t.
Proof.
Opaque tree_remove_root.
induction t; simpl; intros.
subst. simpl. constructor.
destruct (k0 =? k).
subst.
eapply tree_remove_root_bst; try eauto. apply ISBST.
destruct (k0 <? k).
subst.
simpl.
split.
apply remove_satisfies_all. apply ISBST.
split. apply ISBST. split.
eapply IHt1. apply ISBST. eauto. apply ISBST.
subst. simpl.
split. apply ISBST.
split. apply remove_satisfies_all. apply ISBST.
split. apply ISBST.
eapply IHt2; eauto. apply ISBST.
Qed.

Theorem bst_remove_proof : forall t k, is_bst t -> is_bst (tree_remove t k).
Proof.
intros. remember (tree_remove t k) as rm_t.
eapply tree_remove_bst. apply H. symmetry in Heqrm_t. eassumption.
Qed.

Definition remove_BST (tr: BST) (k: K) : BST :=
  match tr with
  | tree t proof_t         => tree (tree_remove t k) (bst_remove_proof t k proof_t)
  end.

Lemma non_exists_tree_min : forall tr k,
  is_bst tr -> tree_min tr k -> tree_search tr k = None.
Proof.
intros tr k IS_BST.
induction tr.
- intros. reflexivity.
- unfold tree_search. remember (k =? k0) as a. destruct a.
  + symmetry in Heqa; apply Nat.eqb_eq in Heqa; subst. intro. inversion H.
  omega.
  + symmetry in Heqa. remember (k <? k0) as b. destruct b. fold tree_search.
    intro. apply IHtr1. apply IS_BST. apply H.
    fold tree_search. intro. apply IHtr2. apply IS_BST. apply H.
Qed.

Lemma non_exists_tree_max : forall tr k,
  is_bst tr -> tree_max tr k -> tree_search tr k = None.
Proof.
intros tr k IS_BST.
induction tr.
- intros. reflexivity.
- unfold tree_search. remember (k =? k0) as a. destruct a.
  + symmetry in Heqa; apply Nat.eqb_eq in Heqa; subst. intro. inversion H.
  omega.
  + remember (k <? k0) as b. destruct b. fold tree_search.
    intro. apply IHtr1. apply IS_BST. apply H.
    fold tree_search. intro. apply IHtr2. apply IS_BST. apply H.
Qed.

Lemma remove_root_no_find_root : forall t1 t2 (k:K) v, is_bst (node k v t1 t2)
  -> tree_search (tree_remove_root (node k v t1 t2)) k = None.
Proof.
Transparent tree_remove_root.
Opaque tree_find_remove_max.
intros. induction t1.
- intros.  assert (AH:= H). simpl in H. simpl. apply non_exists_tree_min.
apply H. apply H.
- intros. simpl.
induction t2; simpl; intros.
+ (* inducting on right subtree, base case *)
  remember (k =? k0) as a; destruct a.
  symmetry in Heqa. apply Nat.eqb_eq in Heqa. simpl in H. subst.
  assert (tree_max (node k0 v0 t1_1 t1_2) k0). apply H. inversion H0. omega.
  remember (k <? k0) as b; destruct b. simpl in H. symmetry in Heqb; apply Nat.ltb_lt in Heqb.
  assert (tree_max (node k0 v0 t1_1 t1_2) k). apply H. assert (k0 < k). apply H0.
  omega. assert (t1_2 = tree_remove_root (node k v t1_2 null)). { simpl. destruct t1_2; try reflexivity. }
  rewrite <- H0 in IHt1_2. apply IHt1_2.  simpl. simpl in H. destruct H.
  split. apply H. split. constructor. split. apply H1. auto.
+ (* neither left nor right subtrees are null *)
  (* annoyingly, too much got unfolded *)
  fold (tree_remove_root (node k v (node k0 v0 t1_1 t1_2) (node k1 v1 t2_1 t2_2))).
  fold (tree_remove_root (node k v (node k0 v0 t1_1 t1_2) t2_2)) in IHt2_2.
  fold (tree_remove_root (node k v (node k0 v0 t1_1 t1_2) t2_1)) in IHt2_1.
  simpl. remember (tree_find_remove_max (node k0 v0 t1_1 t1_2)) as rm_t.
  destruct rm_t.
  remember (node k1 v1 t2_1 t2_2) as rtr.
  remember (node k0 v0 t1_1 t1_2) as ltr.
  clear IHt1_1 IHt1_2 IHt2_1 IHt2_2.
  destruct o.
* (* left subtree has a max *)
  destruct p.
  simpl. simpl in H.
  assert (In (k2, v2) (tree_elements ltr)) as in_left.
  { eapply tree_max_in. eauto. }
  assert (k2 < k) as k2_lt.
  { simpl in H. destruct H. eapply tree_all_keys_elements in in_left; eauto.
  simpl in in_left. assumption. }
  replace (k =? k2) with false.
  replace (k <? k2) with false.
  apply min_no_search.
  apply H.
  remember (k <? k2) as lt. destruct lt. symmetry in Heqlt. apply Nat.ltb_lt in Heqlt. omega. easy.
  symmetry. apply nat_not_equal. intro. omega.
* (* left subtree has no max *)
  assert (ltr <> null) as H'. intro; subst; discriminate.
  apply tree_find_remove_max_nonempty in H'.
  destruct H'. destruct H0.
  rewrite H0 in Heqrm_t. discriminate.
Qed.

Theorem remove_unseachable : forall (tr: BST) k, bst_search (remove_BST tr k) k = None.
Proof.
induction tr; simpl; intros.
Transparent tree_remove. Opaque tree_remove_root. induction t.
- (* trivial case *)
reflexivity.
- (* second case *)
simpl . remember (k =? k0) as a. destruct a.
+ symmetry in Heqa. apply Nat.eqb_eq in Heqa. subst. eapply  remove_root_no_find_root.
  apply i.
+ remember (k <? k0) as a. destruct a. simpl. rewrite <- Heqa. rewrite <- Heqa0.
  apply IHt1. apply i. simpl. rewrite <- Heqa. rewrite <- Heqa0. apply IHt2.  apply i.
Qed.

End REMOVE.

End TREE.

(** Some silly examples :p nothing super fancy here *)
Section examples.

Definition null_nat := null nat.

Lemma sample_is_bst: is_bst (node 5 0 (node 4 0 null_nat null_nat) (node 6 0 null_nat null_nat)).
Proof. simpl. repeat constructor. Qed.

Definition first_bst : BST nat :=
tree (node 5 0 (node 4 0 null_nat null_nat) (node 6 0 null_nat null_nat)) sample_is_bst.

Example insert_check1 : is_bst (node 5 0 (node 4 0 null_nat null_nat) (node 6 0 null_nat null_nat)).
Proof.
remember (BST_insert (BST_insert (BST_insert (null_BST nat) 5 0) 4 0) 6 0) as a_bst.
destruct a_bst. simpl in Heqa_bst. injection Heqa_bst; intros. unfold null_nat. rewrite <- H.
apply i. Qed.

Example simple_example: tree_search (tree_insert (null nat) 5 3) 5 = Some 3.
reflexivity. Qed.

Local Open Scope string_scope.
Variable base_tree: BST string.
Definition big_tree := BST_insert (BST_insert (BST_insert (BST_insert (null_BST string) 5 "totonut") 3 "mahalo") 6 "aloha") 4 "hello".

Example big_tree_search_5: bst_search big_tree 5 = Some "totonut".
Proof.
unfold big_tree.
rewrite bst_insert_skip.
rewrite bst_insert_skip.
rewrite bst_insert_skip.
simpl.
easy. easy. easy. easy.
Qed.

End examples.

author: yichaolemon


text:
From Test Require Import tactic.

Section FOFProblem.

Variable Universe : Set.
Variable UniverseElement : Universe.

Variable wd_ : Universe -> Universe -> Prop.
Variable col_ : Universe -> Universe -> Universe -> Prop.

Variable col_swap1_1 : (forall A B C : Universe, (col_ A B C -> col_ B A C)).
Variable col_swap2_2 : (forall A B C : Universe, (col_ A B C -> col_ B C A)).
Variable col_triv_3 : (forall A B : Universe, col_ A B B).
Variable wd_swap_4 : (forall A B : Universe, (wd_ A B -> wd_ B A)).
Variable col_trans_5 : (forall P Q A B C : Universe, ((wd_ P Q /\ (col_ P Q A /\ (col_ P Q B /\ col_ P Q C))) -> col_ A B C)).

Theorem pipo_6 : (forall A B C D M N Aprime Bprime Cprime Dprime Mprime Nprime H G L K : Universe, ((wd_ N M /\ (wd_ M C /\ (wd_ C D /\ (wd_ N D /\ (wd_ Nprime Mprime /\ (wd_ Mprime Cprime /\ (wd_ Cprime Dprime /\ (wd_ Nprime Dprime /\ (wd_ A B /\ (wd_ B C /\ (wd_ A D /\ (wd_ A C /\ (wd_ B D /\ (wd_ Aprime Bprime /\ (wd_ Bprime Cprime /\ (wd_ Aprime Dprime /\ (wd_ Aprime Cprime /\ (wd_ Bprime Dprime /\ (wd_ Nprime Aprime /\ (wd_ Mprime Bprime /\ (wd_ N A /\ (wd_ M B /\ (wd_ N H /\ (wd_ H G /\ (wd_ N G /\ (wd_ M G /\ (wd_ M H /\ (wd_ N C /\ (wd_ D G /\ (wd_ A H /\ (wd_ N L /\ (wd_ L G /\ (wd_ K H /\ (wd_ N K /\ (wd_ H C /\ (wd_ D M /\ (wd_ M A /\ (wd_ K M /\ (wd_ D H /\ (wd_ Mprime Dprime /\ (wd_ Nprime Cprime /\ (wd_ L H /\ (col_ A D H /\ (col_ H A N /\ (col_ M N L /\ (col_ K M C /\ (col_ C K H /\ (col_ D K H /\ (col_ G K H /\ (col_ Nprime Aprime Dprime /\ (col_ N A D /\ (col_ Mprime Bprime Cprime /\ (col_ M B C /\ col_ N D H))))))))))))))))))))))))))))))))))))))))))))))))))))) -> col_ C D H)).
Proof.
  time tac.
Qed.

End FOFProblem.

author: janicicpredrag

repo: Larus

save_path: github-repos/coq/janicicpredrag-Larus