text:
(* Cyclone Semantics using TLC/LN in Coq Version 4 *)
(* "SAFE PROGRAMMING AT THE C LEVEL OF ABSTRACTION".   Daniel Grossman, August 2003 *)
(* Lemmas from the Lambda JAR paper. *)
(* Brian Milnes 2016 *)

Set Implicit Arguments.
Require Export Cyclone_Type_Substitution Cyclone_LN_FV Cyclone_LN_LC_Body Cyclone_LN_Open_Close Cyclone_LN_Tactics Cyclone_LN_FSET Cyclone_LN_Tactics Cyclone_LN_Size.
Open Scope cyclone_scope.

(* This is the version just for the lemmas about manipulating terms. *)

(* ====================================================================== *)
(** ** Proofs *)

(* ********************************************************************** *)
(** Variable closing and variable opening are reciprocal of one another *)

(** Showing that [close_var] after [open_var] is the identity is easy *)

Lemma close_v_tm_v_open_t_t_v :
  forall t x n,
  x \notin fv_tm_v t ->
  close_rec_v_tm_v n x (open_rec_v_tm_v n x t) = t.
Proof.
  introv.
  induction t; simpl; introv Fr; fequals~.
  case_nat~. simpl. case_var~.
  case_var~.
Qed.

(* BUG: unparallel with p and v on the arguments here. *)

Lemma close_v_tm_p_open_t_t_p :
  forall t x n,
  x \notin fv_tm_p t ->
  close_rec_v_tm_p n x (open_rec_v_tm_p n x t) = t.
Proof.
  introv.
  induction t; simpl; introv Fr; fequals~.
  case_nat~. simpl. case_var~.
  case_var~.
Qed.

(* Restart Here: time for simultaneous induction but the form is working. *)

Lemma close_v_tm_e_open_t_t_e :
  forall t x n,
    x \notin fv_tm_st t ->
    close_rec_v_tm_st n x (open_rec_v_tm_st n x t) = t.
Proof.
  apply (St_ind_mutual
           (fun t : St =>
              forall x n,
                x \notin fv_tm_st t ->
                close_rec_v_tm_st n x (open_rec_v_tm_st n x t) = t)
           (fun t : E  =>
              forall x n,
                x \notin fv_tm_e t ->
                close_rec_v_tm_e n x (open_rec_v_tm_e n x t) = t)
           (fun t : F  =>
              forall x n,
                x \notin fv_tm_f t ->
                close_rec_v_tm_f n x (open_rec_v_tm_f n x t) = t));
  try solve[intros;
            simpl;
            fequals~;
            try apply* close_v_tm_v_open_t_t_v];
  (* A bit sloppy I'd say. *)
  try solve[
  introv IH1 IH2 NI;
  simpl;
  fequals~;
  simpl in NI;
  try solve[applys* IH1];
  try solve[applys* IH2]];
  try solve[
        introv IH1 IH2 IH3 NI;
        simpl;
          fequals~;
                 simpl in NI;
          try solve[applys* IH1];
          try solve[applys* IH2];
          try solve[applys* IH3]].
  all: intros.
  simpl.
  fequals~.
  simpl in H.
  try apply* close_v_tm_v_open_t_t_v.

Qed.

Lemma close_v_tm_open_t_t : forall x t,
  x \notin fv_tm t ->
  close_rec_v_tm 0 x (open_rec_v_tm 0 x t) = t.
Proof.
  introv. generalize 0.
  induction t; simpl; introv Fr; fequals~.
  case_nat~. simpl. case_var~.
  case_var~.
Qed.

(** The other direction is much harder; First, we first need
    to establish the injectivity of [open_var] *)

Lemma open_var_inj :
  forall x t1 t2,
    x \notin (fv_tm t1) ->
    x \notin (fv_tm t2) ->
    open_t_t (fevar x) t1 = open_t_t (fevar x) t2 ->
    (t1 = t2).
Proof.
  introv Fr1 Fr2 Eq.
  rewrite~ <- (@close_v_tm_open_t_t x t1).
  rewrite~ <- (@close_v_tm_open_t_t x t2).
  fequals~.
Qed.

(** We also need one (tricky) auxiliary lemma to handle the binder case *)

Lemma open_close_var_on_open_var :
  forall x y z t i j,
    i <> j ->
    y <> x ->
    y \notin (fv_tm t) ->
    open_rec_t_t i (fevar y) (open_rec_t_t j (fevar z) (close_rec_v_tm j x t))
  = open_rec_t_t j (fevar z) (close_rec_v_tm j x (open_rec_t_t i (fevar y) t)).
Proof.
  induction t; try solve[simpl; intros; try solve [ fequals~ ]];
  intros;
  do 4 (simpl; try case_nat~; try case_nat~; try case_var~).
Qed.

(** Now we can prove that [open_var] after [close_var] is the identity *)

Lemma open_close_var : forall x t,
  lc_t t ->
  open_t_t (fevar x) (close_v_tm x t)  = t.
Proof.
  introv T. unfold open_t_t, close_v_tm. generalize 0.
  induction T; try solve[intros; simpl; introv; fequals~];
  try solve[intros; simpl; case_var~; simpl; case_nat~];
  intros;
  simpl;
  fequals~;
  match goal with
   |- ?t = _ => pick_fresh y from (fv_tm t)
  end;
  apply~ (@open_var_inj y);
  lets M: open_close_var_on_open_var;
  unfold open_t_t in M;
  unfold open_t_t;
  rewrite~ M .
Qed.

(** As a bonus, we get the injectivity of [close_var] *)

Lemma close_var_inj : forall x t1 t2,
  lc_t t1 -> lc_t t2 ->
  close_v_tm x t1 = close_v_tm x t2 ->
  (t1 = t2).
Proof.
  introv T1 T2 Eq.
  rewrite~ <- (@open_close_var x t1).
  rewrite~ <- (@open_close_var x t2).
  fequals~.
Qed.

(* ********************************************************************** *)
(** Properties of [body] *)

(** An abstraction is locally closed iff it satifies the predicate [body] *)

(* BUG: why is this working for Arthur and not me? LC hints ? *)

Lemma lc_utype_iff_body : forall k t,
  lc_t (utype k t) <-> body_t t.
Proof.
  intros.
  unfold body_t, open_t_t.
  iff H;
  inversions* H.
Qed.

Lemma lc_etype_iff_body : forall p k t,
  lc_t (etype p k t) <-> body_t t.
Proof.
  intros.
  unfold body_t, open_t_t.
  iff H; inversions* H.
Qed.

(*
Lemma lc_abs_iff_body : forall t1,
  lc (trm_abs t1) <-> body t1.
Proof. intros. unfold body.
       iff H; inversions* H.
Qed.
*)

(* ********************************************************************** *)
(** Interaction of [fv] with [open_var] and [close_var] *)

(** Opening with [u] adds [fv u] to the set of free variables *)

Lemma ftv_open : forall t u,
  fv_tm (open_t_t u t) \c fv_tm t \u fv_tm u.
Proof.
  introv. unfold open_t_t. generalize 0.
  induction t; intros l; simpl; try case_nat; try fset.
Qed.

(*
Lemma fv_open : forall t u,
  fv (open t u) \c fv t \u fv u.
Proof.
  introv. unfold open. generalize 0.
  induction t; intros k; simpl; try fset.
  case_nat; simpl; fset.
Qed.
*)

(** In particular, opening with variable [x] adds [x] to the set
    of free variables *)

Lemma open_var_fv : forall x t,
  fv_tm (open_rec_t_t 0 (fevar x) t) \c (fv_tm t \u \{x}).
Proof. intros. apply ftv_open. Qed.

(*
Lemma open_var_fv : forall x t,
  fv (open_var t x) \c (fv t \u \{x}).
Proof. intros. apply fv_open. Qed.
*)

(** Closing w.r.t variable [x] removes [x] from the set of free variables *)

Lemma close_tv_fv : forall x t,
  fv_tm (close_rec_v_tm 0 x t) \c (fv_tm t \- \{x}).
Proof.
  introv. unfold close_v_tm. generalize 0.
  induction t; intros l; simpl; try fset.
  case_var; simpl; fset.
Qed.

(*
Lemma close_var_fv : forall x t,
  fv (close_var x t) \c (fv t \- \{x}).
Proof.
  introv. unfold close_var. generalize 0.
  induction t; intros k; simpl; try fset.
  case_var; simpl; fset.
Qed.
*)

(* ********************************************************************** *)
(** Properties of substitution *)

(** Distributivity of [subst] on [open].
    Two (tricky) intermediate lemmas are required *)

Lemma open_rec_lc_ind :
  forall t j v i u,
    i <> j ->
    open_rec_t_t i u (open_rec_t_t j v t) = open_rec_t_t j v t ->
    open_rec_t_t i u t = t.
Proof.
  induction t; introv Nq Eq;
   simpls; inversions~ Eq; fequals*.
  case_nat~. case_nat~.
Qed.

Lemma open_rec_t_t_lc_t : forall u t k,
  lc_t t -> open_rec_t_t k u t = t.
Proof.
  introv T. gen k.
  induction T; intros; simpl; fequals~;
  pick_fresh x;
  apply~ (@open_rec_lc_ind t0 0 (fevar x));
  apply~ H0.
Qed.

Lemma subst_t_v_tm_open_rec_t_t :
  forall x u t v,
    lc_t u ->
    subst_t_v_tm u x (open_rec_t_t 0 v t) =
    open_rec_t_t 0 (subst_t_v_tm u x v) (subst_t_v_tm u x t).
Proof.
  intros. generalize 0.
  induction t; intros; simpl; fequals~.
  case_nat~.
  case_var~. rewrite~ open_rec_t_t_lc_t.
Qed.

(** In particular, we can distribute [subst] on [open_var] *)

Lemma subst_t_v_tm_open_rec_v_tm:
  forall x y u t,
    x <> y ->
    lc_t u ->
    subst_t_v_tm u x (open_rec_t_t 0 (fevar y) t) =
    open_rec_t_t 0 (fevar y) (subst_t_v_tm u x t).
Proof.
  introv N U.
  rewrite~ subst_t_v_tm_open_rec_t_t.
  fequals.
  simpl.
  case_if~.
Qed.

(** For the distributivity of [subst] on [close_var],
    one simple intermediate lemmas is required to
    say that closing on a fresh name is the identity *)

Lemma close_rec_v_tm_fresh : forall k x t,
  x \notin fv_tm t -> close_rec_v_tm k x t = t.
Proof.
  introv. gen k. induction t; simpl; intros; fequals*.
  case_var~.
Qed.

(** Distributivity of [subst] on [close_var] *)

Lemma subst_t_v_tm_close_rec_v_tm:
  forall x y u t,
    x <> y ->
    y \notin fv_tm u ->
    subst_t_v_tm u x (close_rec_v_tm 0 y t) = close_rec_v_tm 0 y (subst_t_v_tm u x t).
Proof.
  introv N F. generalize 0.
  induction t; intros l; simpl; fequals~.
  case_var~; simpl.
  case_var~; simpl. case_var~.
  case_var~; simpl.
  rewrite~ close_rec_v_tm_fresh.
  case_var~.
Qed.

(** Substitution for a fresh name is the identity *)

Lemma subst_t_v_tm_fresh : forall x t u,
  x \notin fv_tm t -> subst_t_v_tm u x t = t.
Proof.
  intros.
  induction t; simpls; fequals~. case_var~.
Qed.

(** Substitution can be introduced to decompose an opening *)

Lemma subst_t_v_tm_intro :
  forall x t u,
    x \notin (fv_tm t) ->
    lc_t u ->
    open_rec_t_t 0 u t = subst_t_v_tm u x (open_rec_t_t 0 (fevar x) t).
Proof.
  introv F U.
  rewrite~ subst_t_v_tm_open_rec_t_t.
  fequals.
  simpl.
  case_var~.
  rewrite~ subst_t_v_tm_fresh.
Qed.

(** An alternative, longer proof, but with fewer hypotheses *)

Lemma subst_t_v_tm_intro_alternative : forall x t u,
  x \notin (fv_tm t) ->
  open_rec_t_t 0 u t = subst_t_v_tm u x (open_rec_t_t 0 (fevar x) t).
Proof.
  introv H. generalize 0. gen H.
  induction t; simpl; intros; fequals*.
  case_nat*.
  simpl. case_var*.
  case_var*.
Qed.

(** Substitution can be introduced to decompose a variable
    closing in terms of another one using a different name *)

Lemma close_v_tm_rename : forall x y t,
  x \notin fv_tm t ->
  close_rec_v_tm 0 y t =
  close_rec_v_tm 0 x (subst_t_v_tm (fevar x) y t).
Proof.
  introv.  generalize 0.
  induction t; simpl; intros l F; fequals~.
  case_var~; case_var~; simpl; case_var~.
Qed.

(* ********************************************************************** *)
(** Preservation of local closure through substitution and opening *)

(** Substitution of a locally closed terms into another one produces
    a locally closed term *)

Lemma subst_lc : forall x u t,
  lc_t u -> lc_t t -> lc_t (subst_t_v_tm u x t).
Proof.
  introv U T. induction T; simple~;
  try case_var~;
  try apply_fresh lc_t_utype;
  try apply_fresh lc_t_etype;
  rewrite~ <- subst_t_v_tm_open_rec_v_tm.
Qed.

(** Substitution of a locally closed terms into a body one produces
    another body *)

Lemma subst_t_v_tm_body_t :
  forall x t u,
    lc_t u -> body_t t -> body_t (subst_t_v_tm u x t).
Proof.
  introv U [L H].
  exists_fresh.
  rewrite~ <- subst_t_v_tm_open_rec_v_tm.
  apply~ subst_lc.
Qed.

(** Opening of a body with a locally closed terms produces a
    locally closed term *)

Lemma open_rec_t_t_preserves_lc_t : forall t u,
  body_t t -> lc_t u -> lc_t (open_rec_t_t 0 u t).
Proof.
  introv [L H] U.
  pick_fresh x.
  rewrite~ (@subst_t_v_tm_intro x).
  apply~ subst_lc.
Qed.

(* ====================================================================== *)
(** ** An induction principle for locally closed terms *)

(** Interaction of [size] with [open_var] *)

Lemma size_open_rec_v_tm : forall x t,
  size_t (open_rec_t_t 0 (fevar x) t) = size_t t.
Proof.
  intros. generalize 0.
  induction t; intros; simple~. case_nat~.
Qed.

(** Interaction of [size] with [close_var] *)

Lemma size_close_var : forall x t,
  size_t (close_rec_v_tm 0 x t) = size_t t.
Proof.
  intros. generalize 0.
  induction t; intros; simple~. case_var~.
Qed.

(** The induction principle *)
(* This would be a bear, let me check and see if I actually do induction on
 the size of types or terms in the thesis.

Lemma lc_induct_size : forall P : trm -> Prop,
  (forall x, P (trm_fvar x)) ->
  (forall t1 t2,
     lc t1 -> P t1 -> lc t2 -> P t2 -> P (trm_app t1 t2)) ->
  (forall t1,
     body t1 ->
     (forall t2 x, x \notin fv t2 -> size t2 = size t1 ->
       lc (open_var t2 x) -> P (open_var t2 x)) ->
     P (trm_abs t1)) ->
  (forall t, lc t -> P t).
Proof.
  intros P Hvar Happ Habs t.
  induction t using (@measure_induction _ size).
  introv T. inverts T; simpl in H; auto.
  apply~ Habs. exists_fresh; auto. introv Fr Eq T.
   apply~ H. rewrite~ size_open_var.
Qed.

*)

author: briangmilnes

repo: CycloneCoqSemantics


text:
(** Formal Reasoning About Programs <http://adam.chlipala.net/frap/>
  * Supplementary Coq material: subset types
  * Author: Adam Chlipala
  * License: https://creativecommons.org/licenses/by-nc-nd/4.0/
  * Much of the material comes from CPDT <http://adam.chlipala.net/cpdt/> by the same author. *)

Require Import FrapWithoutSets.
(* We import a pared-down version of the book library, to avoid notations that
 * clash with some we want to use here. *)

Set Implicit Arguments.
Set Asymmetric Patterns.

(** * Introducing Subset Types *)

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

Extraction pred.

(** * Decidable Proposition Types *)

Print sumbool.

Notation "'Yes'" := (left _ _).
Notation "'No'" := (right _ _).
Notation "'Reduce' x" := (if x then Yes else No) (at level 50).

Definition eq_nat_dec : forall n m : nat, {n = m} + {n <> m}.
Admitted.

Compute eq_nat_dec 2 2.
Compute eq_nat_dec 2 3.

Extraction eq_nat_dec.

Section In_dec.
  Variable A : Set.
  Variable A_eq_dec : forall x y : A, {x = y} + {x <> y}.

  (* The final function is easy to write using the techniques we have developed
   * so far. *)

  Definition In_dec : forall (x : A) (ls : list A), {In x ls} + {~ In x ls}.
  Admitted.
End In_dec.

Compute In_dec eq_nat_dec 2 (1 :: 2 :: nil).
Compute In_dec eq_nat_dec 3 (1 :: 2 :: nil).

Extraction In_dec.

(** * Partial Subset Types *)

Inductive maybe (A : Set) (P : A -> Prop) : Set :=
| Unknown : maybe P
| Found : forall x : A, P x -> maybe P.

Notation "{{ x | P }}" := (maybe (fun x => P)).
Notation "??" := (Unknown _).
Notation "[| x |]" := (Found _ x _).

Print sumor.

Notation "!!" := (inright _ _).
Notation "[|| x ||]" := (inleft _ [x]).

(** * Monadic Notations *)

Notation "x <- e1 ; e2" := (match e1 with
                             | Unknown => ??
                             | Found x _ => e2
                           end)
(right associativity, at level 60).

Definition doublePred : forall n1 n2 : nat, {{p | n1 = S (fst p) /\ n2 = S (snd p)}}.
Admitted.

Notation "x <-- e1 ; e2" := (match e1 with
                               | inright _ => !!
                               | inleft (exist x _) => e2
                             end)
(right associativity, at level 60).

Definition doublePred' : forall n1 n2 : nat,
  {p : nat * nat | n1 = S (fst p) /\ n2 = S (snd p)}.
Admitted.

(** * A Type-Checking Example *)

Inductive exp :=
| Nat (n : nat)
| Plus (e1 e2 : exp)
| Bool (b : bool)
| And (e1 e2 : exp).

Inductive type := TNat | TBool.

Inductive hasType : exp -> type -> Prop :=
| HtNat : forall n,
  hasType (Nat n) TNat
| HtPlus : forall e1 e2,
  hasType e1 TNat
  -> hasType e2 TNat
  -> hasType (Plus e1 e2) TNat
| HtBool : forall b,
  hasType (Bool b) TBool
| HtAnd : forall e1 e2,
  hasType e1 TBool
  -> hasType e2 TBool
  -> hasType (And e1 e2) TBool.

Definition typeCheck : forall e : exp, {{t | hasType e t}}.
Admitted.

Compute typeCheck (Nat 0).
Compute typeCheck (Plus (Nat 1) (Nat 2)).
Compute typeCheck (Plus (Nat 1) (Bool false)).

Extraction typeCheck.

author: svanderbleek

repo: frap-psets


text:
Require Import Core.

Fixpoint find_struct_fields (id : ident) (c : list composite_definition) :=
  match c with
  | [] => []
  | h :: tl => match h with
             | Composite id' _ ls _ =>
               if (id =? id')%positive
               then ls
               else find_struct_fields id tl
             end
  end.

Fixpoint ls_to_seq (ls : list statement) :=
  match ls with
  | [] => Sskip
  | [h] => h
  | h1 :: h2 :: tl => Ssequence h1 (Ssequence h2 (ls_to_seq tl))
  end.

Fixpoint copy_by_fields (p : positive) (e : expr) (id2 : ident) (ty : type) (ls : members) :=
  match ls with
  | [] => []
  | h :: tl => let f := fst h in
             let t := snd h in
             let p' := (p + f)%positive in
             let s :=
                 Ssequence
                   (Sset p' (Efield (Evar id2 ty) f t))
              match e with
                | (Evar id1 ty1) => (Sassign (Efield (Evar id1 ty) f t)
                                            (Etempvar p' t))
                | (Etempvar id1 ty1) => (Sassign (Efield (Etempvar id1 ty) f t)
                                                (Etempvar p' t))
                | (Ederef (Evar id1 ty1) _) =>
                  (Sassign  (Efield (Ederef (Evar id1 (tptr ty)) ty) f t)
                            (Etempvar p' t))
                | (Ederef (Etempvar id1 ty1) _) =>
                  (Sassign  (Efield (Ederef (Etempvar id1 (tptr ty)) ty) f t)
                            (Etempvar p' t))
                | _ => Sskip
              end in
             s :: copy_by_fields p e id2 ty tl
  end.

Fixpoint struct_normalize (s : statement) (c : list composite_definition) (p : positive) :=
  match s with
  | Ssequence s1 s2 =>
    Ssequence (struct_normalize s1 c p) (struct_normalize s2 c p)
  | Sloop s1 s2 => Sloop (struct_normalize s1 c p) (struct_normalize s2 c p)
  | Sifthenelse e s1 s2 => Sifthenelse e (struct_normalize s1 c p) (struct_normalize s2 c p)
  | Sswitch e ls =>
    Sswitch e ((fix switch_normalize ls :=
                  match ls with
                  | LSnil => LSnil
                  | LScons z s ls' => LScons z (struct_normalize s c p) (switch_normalize ls')
                  end) ls)
  | Slabel l s => Slabel l (struct_normalize s c p)
  | Sassign e (Evar id2 ty2) =>
    match ty2 with
    | Tstruct _struct _ =>
      let ls := find_struct_fields _struct c in
      ls_to_seq (copy_by_fields p e id2 (Tstruct _struct noattr) ls)
    | _ => s
    end
  | Scall id e le =>
    match e with
    | Evar v (Tfunction tl t cc) =>
      Scall id (Evar v (Tfunction tl t (mkcallconv (cc_vararg cc)
                                                   (cc_unproto cc) false))) le
    | _ => s
    end
  | s => s
  end.

Definition fresh_ident f :=
   (Z.to_pos (Zlength (fn_temps f)) * last (map fst (fn_temps f)) 1)%positive.

Fixpoint new_fn_temps p fs c :=
match fs with
| [] => []
| h :: tl =>
  (fix new_fn_temps_loop  (f : list (ident * type))  c :=
      match f with
      | [] => []
      | h :: tl =>
        match snd h with
           | Tstruct id _ =>
        let ls := find_struct_fields id c in
        map (fun t => ((fun x => p + x)%positive (fst t), snd t)) ls
                                  ++ new_fn_temps_loop tl c
           | _ => new_fn_temps_loop tl c
        end
      end) h c ++ new_fn_temps p tl c
end.

Definition normalize_function f c :=
  mkfunction (fn_return f)
             {|cc_vararg:= cc_vararg (fn_callconv f);
               cc_unproto := cc_unproto  (fn_callconv f);
               cc_structret:=false|}
             (fn_params f)
             (fn_vars f)
             ((fn_temps f) ++ new_fn_temps (fresh_ident f)
                           [(fn_temps f); (fn_vars f);
                              (fn_params f)] c)
             (struct_normalize (fn_body f) c (fresh_ident f)).

author: asosyuk


text:
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Import ZArith_base.
Require Export Wf_nat.
Require Import Omega.
Local Open Scope Z_scope.

(** Well-founded relations on Z. *)

(** We define the following family of relations on [Z x Z]:

    [x (Zwf c) y]   iff   [x < y & c <= y]
 *)

Definition Zwf (c x y:Z) := c <= y /\ x < y.

(** and we prove that [(Zwf c)] is well founded *)

Section wf_proof.

  Variable c : Z.

  (** The proof of well-foundness is classic: we do the proof by induction
      on a measure in nat, which is here [|x-c|] *)

  Let f (z:Z) := Z.abs_nat (z - c).

  Lemma Zwf_well_founded : well_founded (Zwf c).
    red; intros.
    assert (forall (n:nat) (a:Z), (f a < n)%nat \/ a < c -> Acc (Zwf c) a).
    clear a; simple induction n; intros.
  (** n= 0 *)
    case H; intros.
    case (lt_n_O (f a)); auto.
    apply Acc_intro; unfold Zwf; intros.
    assert False; omega || contradiction.
  (** inductive case *)
    case H0; clear H0; intro; auto.
    apply Acc_intro; intros.
    apply H.
    unfold Zwf in H1.
    case (Z.le_gt_cases c y); intro; auto with zarith.
    left.
    red in H0.
    apply lt_le_trans with (f a); auto with arith.
    unfold f.
    apply Zabs2Nat.inj_lt; omega.
    apply (H (S (f a))); auto.
  Qed.

End wf_proof.

Hint Resolve Zwf_well_founded: datatypes.

(** We also define the other family of relations:

    [x (Zwf_up c) y]   iff   [y < x <= c]
 *)

Definition Zwf_up (c x y:Z) := y < x <= c.

(** and we prove that [(Zwf_up c)] is well founded *)

Section wf_proof_up.

  Variable c : Z.

  (** The proof of well-foundness is classic: we do the proof by induction
      on a measure in nat, which is here [|c-x|] *)

  Let f (z:Z) := Z.abs_nat (c - z).

  Lemma Zwf_up_well_founded : well_founded (Zwf_up c).
  Proof.
    apply well_founded_lt_compat with (f := f).
    unfold Zwf_up, f.
    intros.
    apply Zabs2Nat.inj_lt; try (apply Z.le_0_sub; intuition).
    now apply Z.sub_lt_mono_l.
  Qed.

End wf_proof_up.

Hint Resolve Zwf_up_well_founded: datatypes.

author: Priyanka-Mondal

repo: Coq

save_path: github-repos/coq/Priyanka-Mondal-Coq


text:
Set Implicit Arguments.
Unset Strict Implicit.

Require Import basics.
Require Import enat.
Require Import allen.
Require Import signal.
Require Import compare.

Section borders.

Ltac G x := generalize x.

Ltac BAD := intros BAD; inversion BAD.

(* The general lemma when we have an up event at t *)
Lemma up_allen (p:sig) (t:nat) :
 ~(p t) ->
 (p (S t)) ->
 (exists I, (exists J, (tas t I (not_sig p))
                    /\ (tas (S t) J p)
                    /\ (right I)=(Fix (S t))
                    /\ (left J)=(S t) ))
.
rewrite <- not_sig_def.
intros NotPSt Pt.
G (get_sig NotPSt); intros (I,(tInI,IInNp)).
G (get_sig Pt); intros (J,(StInJ,JInp)).
exists I; exists J.
split;[split|split;[split|split]];auto.
- G(inat_compare (right I) (Fix (S t))); intros [LT|[EQ|GT]];[exfalso|auto|exfalso].
  + case_eq (right I);[intros n R|intros EQ; rewrite EQ in LT; inversion LT].
    G (allen_right tInI); G LT.
    rewrite R; simpl.
    apply ltS_lt_false.
  + cut (in_allen (S t) I).
    * intros StInI.
      G (tas_p (tas_def StInI IInNp)); auto.
    * split;[|auto].
      G (allen_left tInI); auto with arith.
- G(nat_compare (left J) (S t)); intros [LT|[EQ|GT]];[exfalso|auto|exfalso].
  + cut (in_allen t J).
    * intros tInJ.
      G (tas_p (tas_def tInJ JInp)); auto.
    * split;[auto with arith|].
      G (allen_right StInJ); case (right J);[|auto].
      intros n; simpl; auto with arith.
  + case_eq (left J).
    * intros EQ; rewrite EQ in GT; inversion GT.
    * intros n L.
      G (allen_left StInJ); G GT.
      rewrite L; simpl.
      apply ltS_lt_false.
Qed.

Lemma down_allen (p:sig) (t:nat) :
 (p t) ->
 ~(p (S t)) ->
 (exists I, (exists J, (tas t I p)
                    /\ (tas (S t) J (not_sig p))
                    /\ (right I)=(Fix (S t))
                    /\ (left J)=(S t) ))
.
intros Pt NPSt.
rewrite <- not_not in Pt.
G (up_allen (p:=(not_sig p)) (t:=t) Pt NPSt).
intros (I,(J,(tIp,(StJp,(RI,LJ))))).
exists I. exists J.
split; auto.
apply (eq_sig_tas (eq_sig_not_not p) tIp).
Qed.

Lemma up_allen_left (p:sig) (t:nat) :
 ~(p t) ->
 (p (S t)) ->
 (exists I, (in_sig I (not_sig p)) /\ (right I)=(Fix (S t))).
intros NOT IS.
G (up_allen NOT IS).
intros (I,(_,((_,IInp),(_,(RI,_))))).
exists I; split; auto.
Qed.

(* the 4 projections of previous lemmas *)
Lemma up_allen_right (p:sig) (t:nat) :
 ~(p t) ->
 (p (S t)) ->
 (exists I, (in_sig I p) /\ (left I)=(S t)).
intros NotPt PSt.
G (up_allen NotPt PSt).
intros (_,(J,(_,((_,JInp),(_,LI))))).
exists J; auto.
Qed.

Lemma down_allen_left (p:sig) (t:nat) :
 (p t) ->
 ~(p (S t)) ->
 (exists I, (in_sig I p) /\ (right I)=(Fix (S t))).
intros Pt NotPSt.
G (down_allen Pt NotPSt).
intros (I,(_,((_,IInp),(_,(RI,_))))).
exists I; split; auto.
Qed.

Lemma down_allen_right (p:sig) (t:nat) :
 (p t) ->
 ~(p (S t)) ->
 (exists I, (in_sig I (not_sig p)) /\ (left I)=(S t)).
intros Pt NotPSt.
G (down_allen Pt NotPSt).
intros (_,(J,(_,((_,JInp),(_,LI))))).
exists J; auto.
Qed.

(* Applications of previous lemmas *)
Lemma next_down (I:allen) (p:sig) (r:nat) :
 (in_sig I p) ->
 (right I) = (Fix r) ->
 (exists J, (in_sig J (not_sig p)) /\ (left J)=r).
intros IInp RI.
case_eq r.
- intros EQ.
  G (allen_right_gt0 I). rewrite RI, EQ; BAD.
- intros pr EQ.
  rewrite EQ in RI.
  apply (down_allen_right (previous_right_in IInp RI) (bounded_right_out IInp RI)).
Qed.

Lemma in_allen_last_is_right (p:sig) (I:allen) (t:nat) :
 (tas t I p) ->
 ~(p (S t)) ->
 (right I)=(Fix (S t)).
intros (tInI,IInp) NotPSt.
G (tas_p (tas_def tInI IInp)). intros Pt.
G (down_allen_left Pt NotPSt).
intros (II,(IIInP,RII)).
rewrite <- RII.
apply (tas_uniq_right (tas_def tInI IInp)
                      (tas_def (in_allen_previous_right RII) IIInP)).
Qed.

Lemma not_sig_follow (p:sig) (I J:allen) (pr:nat) :
 (in_sig I p) ->
 (in_sig J (not_sig p)) ->
 (left J)=(S pr) ->
 (in_allen pr I) ->
 (right I)=(Fix (left J)).
intros IInp JInNotp LJ prInJ.
rewrite LJ.
apply (in_allen_last_is_right (p:=p) (I:=I) (t:=pr)).
split; auto.
rewrite <- LJ.
apply (in_left JInNotp).
Qed.

Lemma border_left (p:sig) (I:allen) (t1 t2:nat) :
 (tas t2 I p) ->
 ~(p t1) ->
 (p (S t1)) ->
 (t1<t2) ->
 (forall x, (t1 < x) -> (x <= t2) -> (p x)) ->
 (left I)=(S t1).
intros t2Ip NPt1 PSt1 LE SLI.
G (up_allen_right NPt1 PSt1).
intros (II,(IIInp,LII)).
rewrite <- LII.
apply (tas_uniq_left (I2:=II) t2Ip). split; auto.
split.
rewrite LII; apply (lt_leS LE).
apply (in_allen_in_sig_follow_right (p:=p) (t:=(S t1))); auto.
- split; auto.
  rewrite <- LII.
  apply in_allen_left.
- intros x LTx LEx.
  apply SLI; auto.
  apply lt_le; auto.
Qed.

Lemma in_sig_between (p:sig) (I J K:allen) :
 (right J)=(Fix (left I)) ->
 (right I)=(Fix (left K)) ->
 (in_sig J (not_sig p)) ->
 (in_sig K (not_sig p)) ->
 (forall t, (in_allen t I) -> (p t)) ->
 (in_sig I p).
intros JI IK JInNotp KInNotq SLICE.
split;[|split;[|auto]].
- case_eq (left I); auto.
  intros l LI.
  rewrite LI in JI.
  apply (previous_right_in JInNotp JI).
- case_eq (right I); auto.
  intros r RI.
  G IK; rewrite RI; simpl; intros OK. inversion OK.
  apply (in_left KInNotq).
Qed.

Lemma previous_up (I:allen) (p:sig) (pl:nat) :
 (in_sig I p) ->
 (left I) = (S pl) ->
 (exists J, (in_sig J (not_sig p)) /\ (right J)=(Fix (S pl))).
intros IInp LI.
apply down_allen_left.
- apply (previous_left_out IInp LI).
- rewrite not_not_sig_def.
  rewrite <- LI.
  apply (in_left IInp).
Qed.

End borders.

author: NicVolanschi

repo: Allen

save_path: github-repos/coq/NicVolanschi-Allen