text:
From LF Require Export Basics.
From LF Require Export Inductions.

Module NatList.

  Inductive natprod : Type :=
    | pair (n1 n2 : nat).

  Check (pair 3 5).

  Definition fst (p : natprod) : nat :=
    match p with
    | pair a _ => a
    end.

  Definition snd (p : natprod) : nat :=
    match p with
    | pair _ b => b
    end.

  Compute (fst (pair 2 5)).

  Notation "( x , y )" := (pair x y).

  Compute (fst (3, 5)).

  Definition swap_pair (p : natprod) : natprod :=
    match p with
    | (a, b) => (b, a)
    end.

  Theorem surjective_pair :
    forall a b : nat, (a, b) = (fst (a, b), snd (a, b)).
  Proof.
      intros.
      simpl.
      reflexivity.
  Qed.

  Theorem surjective_pair_stuck :
    forall p : natprod, p = (fst p, snd p).
  Proof.
    intros.
    destruct p as [p1 p2] eqn : E.
    reflexivity.
  Qed.

  Theorem snd_fst_is_swap :
    forall p : natprod, (snd p, fst p) = swap_pair p.
  Proof.
    intros p.
    destruct p as [p1 p2].
    simpl.
    reflexivity.
  Qed.

  Theorem fst_swap_is_snd :
    forall (p : natprod), fst (swap_pair p) = snd p.
  Proof.
    intros p.
    destruct p as [p1 p2].
    simpl.
    reflexivity.
  Qed.

  Inductive natlist : Type :=
  | nil
  | cons (n : nat) (l : natlist).

  Definition mylist0 := cons 1 (cons 2 (cons 3 nil)).

  Notation "x :: l" :=
    (cons x l)
    (at level 60, right associativity).

  Notation "[ ]" := nil.

  Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).

  Definition mylist1 := 1 :: (2 :: (3 :: nil)).
  Definition mylist2 := 1 :: 2 :: 3 :: nil.
  Definition mylist3 := 1 :: 2 :: 3 :: [].
  Definition mylist4 := [1; 2; 3].

  Fixpoint repeat (n count : nat) : natlist :=
    match count with
    | O => []
    | S c' => n :: repeat n c'
    end.

  Fixpoint length (n : natlist) : nat :=
    match n with
    | nil => O
    | _ :: n' => S (length n')
    end.

  Fixpoint append (n1 n2 : natlist) : natlist :=
    match n1 with
    | nil => n2
    | e' :: n1' => e' :: (append n1' n2)
    end.

  Notation "x ++ y" := (append x y)
    (at level 60, right associativity).

  Example test_app :
    (append [1; 2; 3] [4; 5; 6]) = [1; 2; 3; 4; 5; 6].
  Proof.
    simpl.
    reflexivity.
  Qed.

  Example test_app_nil_first :
    (append nil [1; 2; 3]) = [1; 2; 3].
  Proof.
    reflexivity.
  Qed.

  Example test_app_nil_second :
    (append [1; 2; 3] nil) = [1; 2; 3].
  Proof.
    simpl.
    reflexivity.
  Qed.

  Definition hd (default : nat) (l : natlist) : nat :=
    match l with
    | nil => default
    | h' :: _ => h'
    end.

  Definition tl (l : natlist) : natlist :=
    match l with
    | nil => nil
    | _ :: l' => l'
    end.

  Fixpoint nonzeros (l : natlist) : natlist :=
    match l with
    | nil => nil
    | O :: l' => nonzeros l'
    | h' :: l' => h' :: nonzeros l'
    end.

  Example test_nonzeros :
    nonzeros [0;1;2;3;0;4] = [1;2;3;4].
  Proof.
    simpl.
    reflexivity.
  Qed.

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

  Fixpoint oddmembers (l : natlist) : natlist :=
    match l with
    | nil => nil
    | h' :: l' =>
      if (odd h') then h' :: oddmembers l'
      else oddmembers l'
    end.

  Example test_oddmembers :
    oddmembers [0;1;2;3;4;5;6] = [1;3;5].
  Proof.
    simpl.
    reflexivity.
  Qed.

  Definition countoddmembers (l : natlist) : nat :=
    length (oddmembers l).

  Example test_countoddmembers_0 :
    countoddmembers [0;2;4;6] = 0.
  Proof.
    compute.
    reflexivity.
  Qed.

  Example test_countoddmembers_3 :
    countoddmembers [1;2;3;4;5] = 3.
  Proof.
    compute.
    reflexivity.
  Qed.

  Example test_countoddmembers_nil :
    countoddmembers nil = 0.
  Proof.
    compute.
    reflexivity.
  Qed.

  Fixpoint alternate (l1 l2 : natlist) : natlist :=
    match l1, l2 with
    | nil, l2' => l2'
    | l1', nil => l1'
    | h1 :: l1', h2 :: l2' => h1 :: h2 :: alternate l1' l2'
    end.

  Example test_alternate_same_len :
    alternate [1;2;3] [4;5;6] = [1;4;2;5;3;6].
  Proof.
    simpl.
    reflexivity.
  Qed.

  Example test_alternate_diff_len1 :
    alternate [1] [2;3;4] = [1;2;3;4].
  Proof.
    simpl.
    reflexivity.
  Qed.

  Example test_alternate_diff_len2 :
    alternate [1;2;3] [4] = [1;4;2;3].
  Proof.
    simpl.
    reflexivity.
  Qed.

  Example test_alternate_nil :
    alternate [1;2;3] nil = [1;2;3].
  Proof.
    simpl.
    reflexivity.
  Qed.

  Example test_alternate_same_elements :
    alternate [1;2] [1;2] = [1;1;2;2].
  Proof.
    simpl.
    reflexivity.
  Qed.

  Fixpoint nat_eq (n1 n2 : nat) : bool :=
    match n1, n2 with
    | O, O => true
    | O, _ => false
    | _, O => false
    | S n1', S n2' => nat_eq n1' n2'
    end.

  Notation "x =? y" := (nat_eq x y)
    (at level 70).

  Definition bag := natlist.

  Fixpoint count (v : nat) (s : bag) : nat :=
    match s with
    | nil => O
    | h :: s' =>
      if h =? v then S (count v s')
      else count v s'
    end.

  Example test_count_3 :
    count 1 [1;2;3;1;4;1] = 3.
  Proof.
    simpl.
    reflexivity.
  Qed.

  Example test_count_0 :
    count 6 [1;2;3;1;4;1] = 0.
  Proof.
    simpl.
    reflexivity.
  Qed.

  Definition sum (a b : bag) : bag :=
    a ++ b.

  Example test_sum1 :
    count 1 (sum [1;2;3] [1;4;1]) = 3.
  Proof.
    simpl.
    reflexivity.
  Qed.

  Definition add (v : nat) (s : bag) : bag :=
    v :: s.

  Example test_add1 :
    count 1 (add 1 [1;4;1]) = 3.
  Proof.
    simpl.
    reflexivity.
  Qed.

  Example test_add2 :
    count 5 (add 1 [1;4;1]) = 0.
  Proof.
    simpl.
    reflexivity.
  Qed.

  Fixpoint member (v : nat) (s : bag) : bool :=
    match s with
    | nil => false
    | h :: s' =>
      if h =? v then true
      else member v s'
    end.

  Example test_member1 :
    member 1 [1;4;1] = true.
  Proof.
    simpl.
    reflexivity.
  Qed.

  Example test_member2 :
    member 2 [1;4;1] = false.
  Proof.
    simpl.
    reflexivity.
  Qed.

  Fixpoint remove_one (v : nat) (l : bag) : bag :=
    match l with
    | nil => nil
    | h :: l' =>
      if h =? v then l'
      else h :: remove_one v l'
    end.

  Example test_remove1 :
    count 5 (remove_one 5 [2;1;5;4;1]) = 0.
  Proof.
    simpl.
    reflexivity.
  Qed.

  Example test_remove_one2:
    count 5 (remove_one 5 [2;1;4;1]) = 0.
  Proof.
    simpl.
    reflexivity.
  Qed.

  Example test_remove_one3:
    count 4 (remove_one 5 [2;1;4;5;1;4]) = 2.
  Proof.
    simpl.
    reflexivity.
  Qed.

  Example test_remove_one4:
    count 5 (remove_one 5 [2;1;5;4;5;1;4]) = 1.
  Proof.
    simpl.
    reflexivity.
  Qed.

  Fixpoint remove_all (v : nat) (s : bag) : bag :=
    match s with
    | nil => nil
    | h :: s' =>
      if h =? v then remove_all v s'
      else h :: remove_all v s'
    end.

  Example test_remove_all1 :
    count 5 (remove_all 5 [2;1;5;4;1]) = 0.
  Proof.
    simpl.
    reflexivity.
  Qed.

  Example test_remove_all2 :
    count 5 (remove_all 5 [2;1;4;1]) = 0.
  Proof.
    simpl.
    reflexivity.
  Qed.

  Example test_remove_all3 :
    count 4 (remove_all 5 [2;1;4;5;1;4]) = 2.
  Proof.
    simpl.
    reflexivity.
  Qed.

  Example test_remove_all4 :
    count 5 (remove_all 5 [2;1;5;4;5;1;4;5;1;4]) = 0.
  Proof.
    simpl.
    reflexivity.
  Qed.

  Fixpoint included (s1 : bag) (s2 : bag) : bool :=
    match s1 with
    | nil => true
    | h :: s' =>
      if member h s2 then included s' (remove_one h s2)
      else false
    end.

  Example test_included1 :
    included [1;2] [2;1;4;1] = true.
  Proof.
    simpl.
    reflexivity.
  Qed.

  Example test_included2 :
    included [1;2;2] [2;1;4;1] = false.
  Proof.
    simpl.
    reflexivity.
  Qed.

  Theorem add_inc_count :
    forall (s : bag) (v : nat),
      count v (add v s) = S (count v s).
  Proof.
  Abort.

  Theorem nil_app :
    forall l : natlist, [] ++ l = l.
  Proof.
    simpl.
    reflexivity.
  Qed.

  Theorem tl_length_pred :
    forall l : natlist, pred (length l) = length (tl l).
  Proof.
    intros.
    induction l as [|l'].
    - simpl.
      reflexivity.
    - simpl.
      reflexivity.
  Qed.

  Theorem tl_length_pred' :
    forall l : natlist, pred (length l) = length (tl l).
  Proof.
    intros.
    destruct l as [|l'].
    - simpl.
      reflexivity.
    - simpl.
      reflexivity.
  Qed.

  Theorem app_assoc :
    forall (l1 l2 l3 : natlist), (l1 ++ l2) ++ l3 = l1 ++ (l2 ++l3).
  Proof.
    intros.
    induction l1 as [|l1'].
    - simpl.
      reflexivity.
    - simpl.
      rewrite IHl1.
      reflexivity.
  Qed.

  Fixpoint rev (l : natlist) : natlist :=
    match l with
    | nil => nil
    | h :: l' => (rev l') ++ [h]
    end.

  Example test_rev1 :
    rev [1;2;3] = [3;2;1].
  Proof.
    simpl.
    reflexivity.
  Qed.

  Example test_rev2 :
    rev nil = nil.
  Proof.
    reflexivity.
  Qed.

  Theorem app_len :
    forall (l1 l2 : natlist), length (l1 ++ l2) = (length l1) + (length l2).
  Proof.
    intros.
    induction l1 as [|l1'].
    - simpl.
      reflexivity.
    - simpl.
      rewrite IHl1.
      reflexivity.
  Qed.

  Theorem rev_length_firsttry :
    forall (l : natlist), length (rev l) = length l.
  Proof.
    induction l as [|n l' IHl'].
    - reflexivity.
    - simpl.
      rewrite <- IHl'.
      rewrite app_len.
      simpl.
      rewrite add_commutative.
      simpl.
      reflexivity.
  Qed.

  Search rev.
  Search (_ + _ = _ + _).
  Search (?x + ?y = ?y + ?x).

  Theorem app_nil_r :
    forall l : natlist, l ++ [] = l.
  Proof.
    induction l as [|l'].
    - reflexivity.
    - simpl.
      rewrite IHl.
      reflexivity.
  Qed.

  Theorem rev_app_distr :
    forall (l1 l2 : natlist), rev (l1 ++ l2) = (rev l2) ++ (rev l1).
  Proof.
    intros.
    induction l1 as [|l1'].
    - simpl.
      rewrite app_nil_r.
      reflexivity.
    - simpl.
      rewrite IHl1.
      rewrite app_assoc.
      reflexivity.
  Qed.

  Theorem rev_involution :
    forall l : natlist, rev (rev l) = l.
  Proof.
    induction l as [|l'].
    - simpl.
      reflexivity.
    - simpl.
      rewrite rev_app_distr.
      rewrite IHl.
      simpl.
      reflexivity.
  Qed.

  Theorem app_assoc4 :
    forall (l1 l2 l3 l4 : natlist),
    l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.
  Proof.
    intros.
    induction l1 as [|l1'].
    - simpl.
      rewrite <- app_assoc.
      reflexivity.
    - simpl.
      rewrite IHl1.
      reflexivity.
  Qed.

  Theorem nonzeros_app :
    forall (l1 l2 : natlist),
    nonzeros (l1 ++ l2) = (nonzeros l1) ++ (nonzeros l2).
  Proof.
    intros.
    induction l1 as [|l1'].
    - simpl.
      reflexivity.
    - destruct l1'.
      -- simpl.
         rewrite IHl1.
         reflexivity.
      -- simpl.
         rewrite IHl1.
         reflexivity.
  Qed.

  Fixpoint eqblist (l1 l2 : natlist) : bool :=
    match l1, l2 with
    | nil, nil => true
    | nil, _ => false
    | _, nil => false
    | h1 :: l1', h2 :: l2' =>
        if h1 =? h2 then eqblist l1' l2'
        else false
    end.

  Example test_eqblist1 :
    (eqblist nil nil) = true.
  Proof.
    simpl.
    reflexivity.
  Qed.

  Example test_eqblist2 :
    (eqblist [1;2;3] [1;2;3]) = true.
  Proof.
    simpl.
    reflexivity.
  Qed.

  Example test_eqblist3 :
    eqblist [1;2;3] [1;2;4] = false.
  Proof.
    simpl.
    reflexivity.
  Qed.

  Theorem eqblist_refl :
    forall (l : natlist), true = eqblist l l.
  Proof.
    intros.
    induction l as [|l'].
    - simpl.
      reflexivity.
    - rewrite IHl.
      induction l' as [|l''].
      -- simpl.
         reflexivity.
      --
  Admitted.

  Theorem count_member_nonzero :
    forall (s : bag), 1 <=? (count 1 (1 :: s)) = true.
  Proof.
    induction s.
    - simpl.
      reflexivity.
    - destruct n.
      --
  Admitted.

  Theorem leb_n_Sn :
    forall (n : nat), n <=? (S n) = true.
  Proof.
    intros.
    induction n as [|n'].
    - simpl.
      reflexivity.
    - simpl.
      rewrite IHn'.
      reflexivity.
  Qed.

  Theorem remove_does_not_increase_count :
    forall (s : bag),
    (count 0 (remove_one 0 s)) <=? (count 0 s) = true.
  Proof.
    intros.
    induction s as [|s'].
    - simpl.
      reflexivity.
    - destruct s'.
      -- simpl.
         rewrite leb_n_Sn.
         reflexivity.
      -- simpl.
         apply IHs.
  Qed.

  Theorem involution_injection :
    forall (f : nat -> nat),
    (forall n : nat, n = f (f n)) -> (forall n1 n2: nat, f n1 = f n2 -> n1 = n2).
  Proof.

  Admitted.

  (* ------- *)
  (* options *)
  (* ------- *)

  Fixpoint nth_bad (l : natlist) (n : nat) : nat :=
    match l with
    | nil => 42
    | a :: l' =>
      match n with
      | O => a
      | S n' => nth_bad l' n'
      end
    end.

  Inductive natoption : Type :=
  | None
  | Some (n : nat).

  Fixpoint nth_err (l : natlist) (n : nat) : natoption :=
    match l with
    | nil => None
    | a :: l' =>
      match n with
      | O => Some a
      | S n' => nth_err l' n'
      end
    end.

  Example test_nth_err1 :
    nth_err [4;5;6;7] 0 = Some 4.
  Proof.
    simpl.
    reflexivity.
  Qed.

  Example test_nth_err2 :
    nth_err [4;5;6;7] 3 = Some 7.
  Proof.
    simpl.
    reflexivity.
  Qed.

  Example test_nth_err3 :
    nth_err [4;5;6;7] 9 = None.
  Proof.
    simpl.
    reflexivity.
  Qed.

  Definition option_elim (default : nat) (o : natoption) : nat :=
    match o with
    | None => default
    | Some v => v
    end.

  Definition hd_err (l: natlist) :natoption :=
    match l with
    | nil => None
    | h :: _ => Some h
    end.

  Example test_hd_err1 :
    hd_err [] = None.
  Proof.
    simpl.
    reflexivity.
  Qed.

  Example test_hd_err2 :
    hd_err [1] = Some 1.
  Proof.
    simpl.
    reflexivity.
  Qed.

  Example test_hd_err3 :
    hd_err [5;6] = Some 5.
  Proof.
    simpl.
    reflexivity.
  Qed.

  Theorem option_elim_hd :
    forall (l : natlist) (default : nat),
    hd default l = option_elim default (hd_err l).
  Proof.
    intros.
    destruct l as [|l'].
    - simpl.
      reflexivity.
    - simpl.
      reflexivity.
  Qed.

  Inductive id : Type :=
  | Id (n : nat).

  Definition eqb_id (x1 x2 : id) :=
    match x1, x2 with
    | Id x1', Id x2' => x1' =? x2'
    end.

  Theorem nat_eqb_refl :
    forall x : nat, x =? x = true.
  Proof.
    intros x.
    induction x as [| x'].
    - simpl.
      reflexivity.
    - simpl.
      rewrite IHx'.
      reflexivity.
  Qed.

  Theorem eqb_id_refl :
    forall x : id, eqb_id x x = true.
  Proof.
    intros.
    destruct x.
    induction n as [|n'].
    - simpl.
      reflexivity.
    - simpl.
      apply nat_eqb_refl.
  Qed.
End NatList.

Module PartialMap.
  Export NatList.

  Inductive partial_map : Type :=
  | empty
  | record (i : id) (v : nat) (m : partial_map).

  Definition update (pm : partial_map) (x : id) (v : nat) : partial_map :=
    record x v pm.

  Fixpoint find (x : id) (pm : partial_map) : natoption :=
    match pm with
    | empty => None
    | record k v pm' =>
      if eqb_id k x then Some v
      else find x pm'
    end.

  Theorem eq_id_refl:
    forall x : id, eqb_id x x = true.
  Proof.
    intros.
    destruct x as [x'].
    simpl.
    apply nat_eqb_refl.
  Qed.

  Lemma nat_eqb_commu:
    forall (a b : nat), (a =? b) = (b =? a).
  Proof.
    induction a as [|a'].
    - destruct b as [|b'].
      -- reflexivity.
      -- simpl.
         reflexivity.
    - intros b.
      destruct b as [|b'].
      -- simpl.
         reflexivity.
      -- simpl.
         rewrite IHa'.
         reflexivity.
  Qed.

  Lemma eqb_id_commu :
    forall (x y : id), eqb_id x y = eqb_id y x.
  Proof.
    intros.
    destruct x. destruct y.
    simpl.
    apply nat_eqb_commu.
  Qed.

  Theorem update_eq :
    forall (pm : partial_map) (i : id) (v : nat),
    find i (update pm i v) = Some v.
  Proof.
    intros.
    destruct pm as [|pm'].
    - simpl.
      rewrite eq_id_refl.
      reflexivity.
    - simpl.
      rewrite eq_id_refl.
      reflexivity.
  Qed.

  Theorem update_neq :
    forall (pm : partial_map) (x y : id) (o : nat),
    eqb_id x y = false -> find x (update pm y o) = find x pm.
  Proof.
    intros.
    destruct pm as [|pm'].
    - simpl.
      rewrite eqb_id_commu.
      rewrite H.
      reflexivity.
    - simpl.
      rewrite eqb_id_commu.
      rewrite H.
      reflexivity.
  Qed.

  Inductive baz : Type :=
  | Baz1 (x : baz)
  | Baz2 (y : baz) (b : bool).

  (* How many elements does the type baz have? *)

End PartialMap.

repo: SoftwareFoundations


text:
(* begin hide *)
Require Import Coq.ZArith.BinInt.
Require Import Coq.Relations.Relations.
Require Import Coq.Lists.List.
Require Import Aniceto.List.
Require Import Aniceto.Map.
Require Import Aniceto.ListSet.
Require Import HJ.Tid.
Require Import HJ.Vars.
Require Import HJ.Phasers.Lang.

Open Scope Z.

(* end hide *)

Section PhDiff.

(**
  The task displacement over phasers is given by predicate [ph_diff] that given
  a phaser [ph], a task [t1], and a task [t2] yields some displacement [z].
  *)

Inductive ph_diff (ph:phaser): (tid * tid) -> Z -> Prop :=
  ph_diff_def:
    forall t1 t2 v1 v2,
    Map_TID.MapsTo t1 v1 ph ->
    Map_TID.MapsTo t2 v2 ph ->
    ph_diff ph (t1, t2) ((Z_of_nat (wait_phase v1)) - (Z_of_nat (wait_phase v2)))%Z.

(* begin hide *)
Hint Resolve ph_diff_def.
(* end hide *)

(** Function [get_ph_diff] implements  predicate [ph_diff]. *)

Definition get_ph_diff (ph:phaser) (t1:tid) (t2:tid) : option Z :=
  match Map_TID.find t1 ph with
    | Some v1 =>
      match Map_TID.find t2 ph with
        | Some v2 =>
          Some ((Z_of_nat (wait_phase v1)) - (Z_of_nat (wait_phase v2)))%Z
        | _ => None
      end
    | _ => None
  end.

(* begin hide *)

Lemma get_ph_diff_spec_1:
  forall ph t1 t2 z,
  get_ph_diff ph t1 t2 = Some z ->
  ph_diff ph (t1, t2) z.
Proof.
  intros.
  unfold get_ph_diff in *.
  remember (Map_TID.find t1 ph).
  symmetry in Heqo.
  destruct o.
  - rewrite <- Map_TID_Facts.find_mapsto_iff in Heqo.
    remember (Map_TID.find t2 ph).
    symmetry in Heqo0.
    destruct o.
    + rewrite <- Map_TID_Facts.find_mapsto_iff in Heqo0.
      inversion H.
      auto.
    + inversion H.
  - inversion H.
Qed.

Lemma get_ph_diff_spec_2:
  forall ph t1 t2 z,
  ph_diff ph (t1, t2) z ->
  get_ph_diff ph t1 t2 = Some z.
Proof.
  intros.
  inversion H; subst; clear H.
  unfold get_ph_diff.
  rewrite Map_TID_Facts.find_mapsto_iff in H2, H4.
  rewrite H2, H4.
  auto.
Qed.

(* end hide *)

(** The main result for [ph_diff] is the proof of correctness. *)

Lemma get_ph_diff_spec:
  forall ph t1 t2 z,
  get_ph_diff ph t1 t2 = Some z <-> ph_diff ph (t1, t2) z.
Proof.
  intros.
  split.
  - apply get_ph_diff_spec_1.
  - apply get_ph_diff_spec_2.
Qed.

(* begin hide *)

Lemma get_ph_diff_spec_none:
  forall ph t1 t2,
  get_ph_diff ph t1 t2 = None <-> (~ Map_TID.In t1 ph \/ ~ Map_TID.In t2 ph).
Proof.
  intros.
  unfold get_ph_diff.
  remember (Map_TID.find (elt:=taskview) t1 ph) as o1.
  symmetry in Heqo1.
  remember (Map_TID.find (elt:=taskview) t2 ph) as o2.
  symmetry in Heqo2.
  destruct o1.
  - destruct o2.
    + split.
      intros.
      * inversion H.
      * intros.
        rewrite <- Map_TID_Facts.find_mapsto_iff in *.
        apply Map_TID_Extra.mapsto_to_in in Heqo1.
        apply Map_TID_Extra.mapsto_to_in in Heqo2.
        destruct H; contradiction H.
    + split.
      * intros.
        right.
        apply Map_TID_Facts.not_find_in_iff.
        assumption.
      * trivial.
  - split.
    + intros.
      left.
      apply Map_TID_Facts.not_find_in_iff.
      assumption.
    + trivial.
Qed.

Lemma get_diff_none:
  forall ph t t',
  get_ph_diff ph t t' = None ->
  forall z, ~ ph_diff ph (t, t') z.
Proof.
  intros.
  intuition.
  apply get_ph_diff_spec_2 in H0.
  rewrite H in H0.
  inversion H0.
Qed.

Lemma ph_diff_fun:
  forall ph t t' z z',
  ph_diff ph (t, t') z ->
  ph_diff ph (t, t') z' ->
  z = z'.
Proof.
  intros.
  apply get_ph_diff_spec_2 in H.
  apply get_ph_diff_spec_2 in H0.
  rewrite H in H0.
  inversion H0.
  trivial.
Qed.

(* end hide *)

(** The reflexive task displacement over a phaser is zero. *)

Lemma ph_diff_refl:
  forall t ph,
  Map_TID.In t ph ->
  ph_diff ph (t, t) 0.
Proof.
  intros.
  apply Map_TID_Extra.in_to_mapsto in H.
  destruct H as (v, H).
  assert (ph_diff ph (t, t) (Z.of_nat (wait_phase v) - Z.of_nat (wait_phase v))) by auto.
  assert ((Z.of_nat (wait_phase v) - Z.of_nat (wait_phase v)) = 0). { intuition. }
  rewrite H1 in *.
  assumption.
Qed.

(** The displacement between two tasks over a phaser is symmetric. *)

Lemma ph_diff_symm:
  forall ph t t' z,
  ph_diff ph (t, t') z ->
  ph_diff ph (t', t) (-z).
Proof.
  intros.
  inversion H; subst; clear H.
  remember (Z.of_nat (wait_phase v1)) as z1.
  remember (Z.of_nat (wait_phase v2)) as z2.
  assert (- (z1 - z2) = z2 - z1). { intuition. }
  rewrite H.
  subst.
  auto.
Qed.

(* begin hide *)

Lemma ph_diff_inv:
  forall ph t t' z,
  ph_diff ph (t, t') z ->
  Map_TID.In t ph /\ Map_TID.In t' ph.
Proof.
  intros.
  inversion H; subst; clear H.
  split.
  - exists v1.
    intuition.
  - exists v2.
    intuition.
Qed.

Lemma ph_diff_inv_left:
  forall ph t t' z,
  ph_diff ph (t, t') z ->
  Map_TID.In t ph.
Proof.
  intros.
  apply ph_diff_inv in H.
  intuition.
Qed.

Lemma ph_diff_inv_right:
  forall ph t t' z,
  ph_diff ph (t, t') z ->
  Map_TID.In t' ph.
Proof.
  intros.
  apply ph_diff_inv in H.
  intuition.
Qed.

Lemma ph_diff_refl_inv:
  forall ph t z,
  ph_diff ph (t, t) z ->
  z = 0 % Z.
Proof.
  intros.
  assert (ph_diff ph (t, t) 0). {
    apply ph_diff_inv_left in H.
    auto using ph_diff_refl.
  }
  eauto using ph_diff_fun.
Qed.

(* end hide *)

(**
  Any two tasks mentioned in a phaser are related with [ph_diff], that is
  there is a displacement between them.
  *)

Lemma ph_diff_total:
  forall ph t t',
  Map_TID.In t ph ->
  Map_TID.In t' ph ->
  exists z, ph_diff ph (t, t') z.
Proof.
  intros.
  apply Map_TID_Extra.in_to_mapsto in H.
  apply Map_TID_Extra.in_to_mapsto in H0.
  destruct H as (v, Hmt).
  destruct H0 as (v', Hmt').
  exists (Z.of_nat (wait_phase v) - Z.of_nat (wait_phase v')).
  auto.
Qed.

(**
  We are now ready to define a less-than operator over a phaser.
  *)

Inductive ph_le (ph : phaser) t t' : Prop :=
  ph_le_def :
    forall z,
    ph_diff ph (t,t') z ->
    (z <= 0)%Z ->
    ph_le ph t t'.

(* begin hide *)

Hint Resolve ph_le_def.

Section GET_PH_LE.
Variable ph:phaser.
Variable t1:tid.
Variable t2:tid.

Inductive ph_le_result :=
  | ph_le_result_ok_l : {z:Z | ph_diff ph (t1, t2) z /\ (z <= 0) % Z } -> ph_le_result
  | ph_le_result_ok_r : {z:Z | ph_diff ph (t2, t1) z /\ (z <= 0) % Z } -> ph_le_result
  | ph_le_fail : {_:unit | ~ Map_TID.In t1 ph \/ ~ Map_TID.In t2 ph } -> ph_le_result.

Program Definition get_ph_le : ph_le_result :=
  match get_ph_diff ph t1 t2 with
    | Some z =>
      if ZArith_dec.Z_le_dec z 0%Z then
        ph_le_result_ok_l z
      else ph_le_result_ok_r (-z)%Z
    | _ => ph_le_fail tt
  end.
Next Obligation.
  intuition.
  symmetry in Heq_anonymous.
  rewrite get_ph_diff_spec in Heq_anonymous.
  assumption.
Defined.
Next Obligation.
  symmetry in Heq_anonymous.
  rewrite get_ph_diff_spec in Heq_anonymous.
  apply ph_diff_symm in Heq_anonymous.
  intuition.
Qed.
Next Obligation.
  remember (get_ph_diff ph t1 t2).
  destruct o.
  - assert (Hx := H z).
    contradiction Hx.
    trivial.
  - symmetry in Heqo.
    apply get_ph_diff_spec_none.
    assumption.
Qed.
End GET_PH_LE.

(* end hide *)

Lemma ph_le_refl:
  forall t ph,
  Map_TID.In t ph ->
  ph_le ph t t.
Proof.
  intros.
  apply ph_le_def with (z:=0%Z); intuition.
  auto using ph_diff_refl.
Qed.

Lemma ph_le_inv:
  forall t t' ph,
  ph_le ph t t' ->
  Map_TID.In t ph /\ Map_TID.In t' ph.
Proof.
  intros.
  inversion H; subst.
  eauto using ph_diff_inv.
Qed.

Lemma ph_le_inv_in:
  forall t t' ph,
  ph_le ph t t' ->
  Map_TID.In t ph /\ Map_TID.In t' ph.
Proof.
  intros.
  inversion H; subst.
  apply ph_diff_inv in H0.
  intuition.
Qed.

Lemma ph_le_inv_in_left:
  forall t t' ph,
  ph_le ph t t' ->
  Map_TID.In t ph.
Proof.
  intros.
  apply ph_le_inv_in in H.
  intuition.
Qed.

Lemma ph_le_inv_in_right:
  forall t t' ph,
  ph_le ph t t' ->
  Map_TID.In t' ph.
Proof.
  intros.
  apply ph_le_inv_in in H.
  intuition.
Qed.

Lemma ph_le_total:
  forall ph t t',
  Map_TID.In t ph ->
  Map_TID.In t' ph ->
  { ph_le ph t t' } + { ph_le ph t' t }.
Proof.
  intros.
  remember (get_ph_le ph t t').
  destruct p.
  - left.
    destruct s as (z, (Hdiff, Hle)).
    eauto.
  - right.
    destruct s as (z, (Hdiff, Hle)).
    eauto.
  - destruct s.
    assert (False). {
      destruct o.
      + contradiction H.
      + contradiction H0.
    }
    inversion H1.
Qed.
End PhDiff.

Section PM_DIFF.
Variable pm:phasermap.

Inductive pm_diff e z: Prop :=
  pm_diff_def :
    forall p ph,
    Map_PHID.MapsTo p ph pm ->
    ph_diff ph e z ->
    pm_diff e z.

Hint Resolve pm_diff_def.

Lemma pm_diff_symm:
  forall t t' z,
  pm_diff (t, t') z ->
  pm_diff (t', t) (-z)%Z.
Proof.
  intros.
  inversion H; subst; clear H.
  eauto using ph_diff_symm.
Qed.

Variable t1: tid.
Variable t2: tid.

Definition all_ph_diffs : phasermap :=
  Map_PHID_Extra.filter
    (fun (p:phid) (ph:phaser) =>
      match (get_ph_diff ph t1 t2) with
        | Some _ => true
        | _ => false
      end)
  pm.

Definition get_pm_diff : option Z :=
  match Map_PHID.elements all_ph_diffs with
    | (p, ph) :: _ => get_ph_diff ph t1 t2
    | _ => None
  end.

Lemma get_pm_diff_eq:
  forall p ph l,
  (p, ph) :: l = Map_PHID.elements (elt:=phaser) all_ph_diffs ->
  Map_PHID.MapsTo p ph pm /\ exists z, ph_diff ph (t1, t2) z.
Proof.
  intros.
  assert (Hmt: Map_PHID.MapsTo p ph all_ph_diffs). {
    apply Map_PHID_Extra.in_elements_impl_maps_to.
    rewrite <- H.
    apply in_eq.
  }
  unfold all_ph_diffs in *.
  rewrite Map_PHID_Extra.filter_spec in Hmt. {
    destruct Hmt.
    intuition.
    remember (get_ph_diff ph t1 t2).
    destruct o.
    - symmetry in Heqo.
      rewrite get_ph_diff_spec in *.
      exists z.
      trivial.
    - inversion H1.
  }
  intuition.
Qed.

Lemma get_pm_diff_spec_1:
  forall z,
  get_pm_diff = Some z ->
  pm_diff (t1, t2) z.
Proof.
  intros.
  unfold get_pm_diff in *.
  remember (Map_PHID.elements all_ph_diffs).
  destruct l.
  { inversion H. }
  destruct p as (p, ph).
  apply get_pm_diff_eq in Heql.
  destruct Heql as (?, _).
  apply get_ph_diff_spec in H.
  eauto.
Qed.

Lemma pm_diff_refl:
  forall t p ph,
  Map_PHID.MapsTo p ph pm ->
  Map_TID.In t ph ->
  pm_diff (t, t) 0.
Proof.
  intros.
  assert (ph_diff ph (t, t) 0). {
    auto using ph_diff_refl.
  }
  eauto.
Qed.

Lemma pm_diff_refl_inv:
  forall t z,
  pm_diff (t, t) z ->
  z = 0 % Z.
Proof.
  intros.
  inversion H; subst; clear H.
  eauto using ph_diff_refl_inv.
Qed.

Variable pm_diff_fun:
  forall e z z',
  pm_diff e z ->
  pm_diff e z' ->
  z = z'.

Lemma get_pm_diff_spec_2:
  forall z,
  pm_diff (t1, t2) z ->
  get_pm_diff = Some z.
Proof.
  intros.
  unfold get_pm_diff.
  remember (Map_PHID.elements all_ph_diffs).
  destruct l.
  - (* absurd case *)
    symmetry in Heql.
    apply Map_PHID_Props.elements_Empty in Heql.
    inversion H; subst; clear H.
    apply Map_PHID_Extra.empty_to_mapsto with (k:=p) (e:=ph) in Heql.
    unfold all_ph_diffs in *.
    rewrite Map_PHID_Extra.filter_spec in Heql. {
      remember (get_ph_diff ph t1 t2).
      destruct o; intuition.
      symmetry in Heqo.
      apply get_diff_none with (z:=z) in Heqo.
      contradiction H1.
    }
    intuition.
  - destruct p as (p, ph).
    apply get_pm_diff_eq in Heql.
    destruct Heql as (?, (z', ?)).
    assert (pm_diff (t1, t2) z'). { eauto using pm_diff_def. }
    assert (z = z'). { eauto using pm_diff_fun. }
    subst.
    apply get_ph_diff_spec.
    trivial.
Qed.

Lemma get_pm_diff_spec:
  forall z,
  get_pm_diff = Some z <-> pm_diff (t1, t2) z.
Proof.
  intros.
  split.
  - apply get_pm_diff_spec_1.
  - apply get_pm_diff_spec_2.
Qed.
End PM_DIFF.

Section LE.
Variable pm:phasermap.

(** Less-than-equals *)
Inductive wp_le t t' : Prop :=
  wp_le_def :
    forall z,
    pm_diff pm (t, t') z ->
    (z <= 0 ) % Z ->
    wp_le t t'.

Hint Resolve wp_le_def.

Lemma wp_le_spec:
  forall t t',
  wp_le t t' <-> (exists z : Z, pm_diff pm (t, t') z /\ (z <= 0)%Z).
Proof.
  intros.
  split.
  + intros.
    inversion H.
    subst.
    exists z.
    intuition.
  + intros.
    destruct H as (z, (Hd, Hle)).
    eauto.
Qed.

Lemma wp_le_def_2:
  forall p ph t t',
  Map_PHID.MapsTo p ph pm ->
  ph_le ph t t' ->
  wp_le t t'.
Proof.
  intros.
  inversion H0; subst.
  eauto using pm_diff_def.
Qed.

Lemma wp_le_alt :
  forall t t',
  wp_le t t' <->
  exists p ph, Map_PHID.MapsTo p ph pm /\ ph_le ph t t'.
Proof.
  split.
  - intros.
    inversion H.
    subst.
    inversion H0.
    subst.
    exists p; exists ph.
    intuition.
    eauto using ph_le_def.
  - intros.
    destruct H as (p, (ph, (Hmt, Hle))).
    inversion Hle; subst.
    eauto using pm_diff_def.
Qed.

Lemma wp_le_refl:
  forall t,
  In t pm ->
  wp_le t t.
Proof.
  intros.
  apply wp_le_def with (z:=0%Z).
  - inversion H.
    eauto using pm_diff_def, ph_diff_refl.
  - intuition.
Qed.

Lemma wp_le_inv:
  forall t t',
  wp_le t t' ->
  In t pm /\ In t' pm.
Proof.
  intros.
  apply wp_le_alt in H.
  destruct H as (p, (ph, (Hmt, Hin))).
  apply ph_le_inv in Hin.
  destruct Hin.
  eauto using in_def.
Qed.

Lemma wp_le_total:
  forall p ph t t',
  Map_PHID.MapsTo p ph pm ->
  Map_TID.In t ph ->
  Map_TID.In t' ph ->
  { wp_le t t' } + { wp_le t' t }.
Proof.
  intros.
  destruct (ph_le_total _ _ _ H0 H1).
  + left.
    eauto using wp_le_def_2.
  + right.
    eauto using wp_le_def_2.
Qed.

Definition LE := clos_trans tid wp_le.

Lemma LE_refl:
  forall t,
  In t pm ->
  LE t t.
Proof.
  intros.
  unfold LE.
  auto using t_step, wp_le_refl.
Qed.

Lemma LE_inv:
  forall t t',
  LE t t' ->
  In t pm /\ In t' pm.
Proof.
  intros.
  unfold LE in H.
  induction H; repeat (eauto using wp_le_inv; intuition).
Qed.

Lemma LE_trans:
  forall t1 t2 t3,
  LE t1 t2 ->
  LE t2 t3 ->
  LE t1 t3.
Proof.
  intros.
  apply t_trans with (y:=t2); repeat auto.
Qed.

Lemma LE_total:
  forall p ph t t',
  Map_PHID.MapsTo p ph pm ->
  Map_TID.In t ph ->
  Map_TID.In t' ph ->
  { LE t t' } + { LE t' t }.
Proof.
  intros.
  unfold LE.
  destruct (wp_le_total _ _ _ _ H H0 H1); repeat (auto using t_step).
Qed.

End LE.

author: cogumbreiro

repo: habanero-coq


text:
Require Import language.
Require Import msl.base.
Require Import msl.seplog.
Require Import msl.alg_seplog.
Require Import seplogic.
Require Import msl.Coqlib2.
Require Import msl.log_normalize.
Require Import msl.eq_dec.

Local Open Scope logic.

Declare Module Semax : SEMAX.
 (* Remark:  "Declare Module" is a hack.
  We want to emphasize that the client proofs (in lseg.v, client_lemmas.v,
   and sample_program.v) can be done independently of the
   model.v that implements the Module Semax.  The correct way to do
   this in Coq is to use a parameterized Module (that is, a Functor),
   which is not difficult but in this example we wanted to avoid
   a heavyweight use of the module system. *)

Import Semax.

Definition next e1 e2: mpred := !! (e1 > 0) && mapsto e1 e2.

Lemma next_gt_0:
  forall x y, next x y = !! (x>0) && next x y.
Proof.
 intros. unfold next.
 rewrite <- andp_assoc. f_equal. rewrite andp_dup. auto.
Qed.

Lemma next_neq_0: forall y, next 0 y |-- FF.   (* W1 *)
Proof.
 intros. rewrite next_gt_0. normalize. inv H.
Qed.

Definition listcons' (R: (adr * adr) -> mpred) (lp: adr * adr) : mpred :=
      !! (fst lp <> snd lp) && EX tail:adr, next (fst lp) tail * |> R (tail, snd lp).

Definition listempty (lp: adr*adr) : mpred :=
             !! (fst lp = snd lp) && emp.

Definition listrep' (R: adr*adr -> mpred) (lp: adr*adr) : mpred :=
        listcons' R lp || listempty lp.

Definition listrep : adr*adr -> mpred := HORec listrep'.

Definition lseg (e1 e2: adr) : mpred := listrep (e1,e2).

Lemma lseg_unfold: forall e1 e2,
   (lseg e1 e2 = (!! (e1<> e2)  && EX tail:adr, next e1 tail * |> lseg tail e2)
                        || (!! (e1=e2) && emp)).
Proof.
 intros.
 unfold lseg. unfold listrep at 1.
 rewrite HORec_fold_unfold. reflexivity.
 unfold listrep', listcons'.
 apply prove_HOcontractive. auto 50 with contractive typeclass_instances.
Qed.

Lemma lseg_neq: forall p q: adr, p<>q ->
        lseg p q = EX y:adr, next p y *  |> lseg y q.
Proof.
 intros.
 apply pred_ext.
 rewrite lseg_unfold at 1.
 apply orp_left.
 normalize. apply exp_right with tail. auto.
 normalize.
 normalize; intro y.
 rewrite (lseg_unfold p q). apply orp_right1.
 normalize. apply exp_right with y. normalize.
Qed.

Lemma lseg_eq: forall a, lseg a a = emp.
Proof.
 intros. rewrite lseg_unfold.
 apply pred_ext.
 apply orp_left.
 normalize.  congruence.
 normalize.
 apply orp_right2. normalize.
Qed.

Lemma lseg_cons: (* U2 *)
 forall x y z, x<>z -> next x y * lseg y z |-- lseg x z.
Proof.
 intros.
 pattern lseg at 1; rewrite lseg_unfold.
 apply orp_right1.
 normalize.
 apply exp_right with y.
 normalize.
 apply sepcon_derives; auto.
 apply now_later.
Qed.

Lemma lseg_neq_0:  forall y, lseg 0 y |-- !! (y=0).  (* W2 *)
Proof.
  intros.
  rewrite lseg_unfold.
 apply orp_left.
 apply andp_left2.
 apply exp_left; intro v.
 rewrite next_gt_0.
 normalize. inv H.
 normalize.
Qed.

Lemma next_lseg:  (* U1 *)
  forall x y, x<>y ->  next x y |-- lseg x y.
Proof.
  intros.
  rewrite <- (sepcon_emp (next x _)).
  rewrite <- (lseg_eq y).
  eapply derives_trans; [ apply lseg_cons | ]; auto.
Qed.

Lemma next_conflict:  (*  W3 *)
   forall x y y', next x y * next x y' |-- FF.
Proof.
  unfold next; intros.
  eapply derives_trans; [ | apply (mapsto_conflict x y y')].
  apply sepcon_derives; apply andp_left2; auto.
Qed.

 Lemma next_conflict_list: (* W4 *)
     forall x y z, next x y * lseg z 0 |-- !!(x<>z).
 Proof.
   intros.
  apply not_prop_right. intro; subst z.
   rewrite lseg_unfold.
  rewrite sepcon_comm.
  rewrite distrib_orp_sepcon.
  apply orp_left.
  normalize.
  rewrite sepcon_comm.
  rewrite <- sepcon_assoc.
  eapply derives_trans with (FF * TT).
  apply sepcon_derives; normalize.
  apply next_conflict.
  normalize.
  unfold next;   normalize.
  inv H.
Qed.

Lemma lseg_W5: forall x y z,   (* W5 *)
    lseg x y * lseg x z |-- !!(x=y \/ x=z).
Proof.
  intros.
  destruct (eq_dec x y).
  apply prop_right; auto.
  destruct (eq_dec x z).
  apply prop_right; auto.
  rewrite (lseg_neq x y); auto.
  rewrite exp_sepcon1; apply exp_left; intro.
  rewrite (lseg_neq x z); auto.
  rewrite exp_sepcon2; apply exp_left; intro.
  rewrite sepcon_assoc.
  rewrite <- (sepcon_assoc (|> _)).
  rewrite (sepcon_comm (|> _)).
  repeat rewrite <- sepcon_assoc. rewrite sepcon_assoc.
  eapply derives_trans. apply sepcon_derives. apply next_conflict. apply derives_refl.
  rewrite FF_sepcon. normalize.
Qed.

Lemma unfash_andp_distrib:
        forall {A}{ND: NatDed A}{IA: Indir A}{RA: RecIndir A} (P: Triv) (Q R: A),
               !P && (Q && R) = (!P && Q) && (!P && R).
Proof.
intros. apply pred_ext;  repeat apply andp_right.
apply andp_left1; auto. apply andp_left2; apply andp_left1; auto.
apply andp_left1; auto. apply andp_left2; apply andp_left2; auto.
apply andp_left1; auto. apply andp_left1; auto.
apply andp_left1; auto. apply andp_left2; auto.
apply andp_left2; auto. apply andp_left2; auto.
Qed.

Lemma lseg_cons_in_next_context:   (*  U4 *)
    forall x y z v, lseg x y * next y z * next z v |-- lseg x z * next z v.
Proof.
  intros.
  apply derives_trans with (((lseg x y * next y z) && (ewand (next z v) TT)) *  next z v).
  apply exclude_elsewhere.
  generalize (goedel_loeb (ALL x:adr,
    lseg x y * next y z && ewand (next z v) TT >=> lseg x z) TT) ; intro.
  spec H.
Focus 2.
  apply sepcon_derives; auto.
  apply subp_e.
  eapply derives_trans; [ apply H |].
  apply allp_left with x. auto.
  clear.
  apply allp_right; intro x.
  apply subp_i1.
  rewrite (lseg_unfold x z).
  apply orp_right1.
  apply andp_right.
  apply not_prop_right; intro; subst x.
  apply andp_left2.
  apply derives_trans with ((EX u:_, (next z u * TT)) && ewand (next z v) TT).
  apply andp_derives.
  rewrite lseg_unfold.
  rewrite distrib_orp_sepcon.
  apply orp_left; normalize.
  apply exp_right with tail. rewrite sepcon_assoc. apply sepcon_derives; normalize.
  apply exp_right with z. apply sepcon_TT. auto.
  normalize.
  apply ewand_conflict.
  rewrite sepcon_comm.
  rewrite <- sepcon_assoc.
  apply derives_trans with (FF * TT); [ | normalize].
  apply sepcon_derives; auto.
  apply next_conflict.

   normalize.
   match goal with |- ! ?P && _ |-- _ => remember P as S end.
   rewrite (lseg_unfold x y).
   rewrite andp_comm.
  rewrite distrib_orp_sepcon.
  rewrite distrib_orp_andp.
  rewrite distrib_orp_andp.
  apply orp_left. normalize. apply exp_right with tail.
  apply derives_trans with (next x tail * (|>lseg tail y * next y z && ewand (next z v) TT && !S)).
  rewrite andp_comm. rewrite <- andp_assoc.
  rewrite sepcon_assoc.
  rewrite unfash_sepcon_distrib.
  eapply derives_trans; [eapply ewand_TT_sepcon | ].
  apply sepcon_derives; auto.
  apply andp_left1. apply andp_left2; auto.
  subst S.
  apply andp_right. apply andp_right. apply andp_left1. apply andp_left2; auto.
  apply andp_left2; auto.
  apply andp_left1; auto. apply andp_left1;auto.
  apply sepcon_derives; auto.
  apply derives_trans with (|> (lseg tail y * next y z && ewand (next z v) TT) && !S).
  apply andp_derives; auto.
  repeat rewrite later_andp. rewrite later_sepcon.
  apply andp_derives; auto. apply sepcon_derives; auto.
   apply now_later. apply now_later.
  subst.
  rewrite <- later_unfash.
  rewrite <- later_andp. apply later_derives.
  apply derives_trans with (lseg tail y * next y z && ewand (next z v) TT &&
           !( lseg tail y * next y z && ewand (next z v) TT >=> lseg tail z)).
 apply andp_derives; auto.
 apply unfash_derives.
 apply allp_left with tail. auto.
 eapply derives_trans; [ eapply andp_derives; [ apply derives_refl | apply unfash_fash] | ].
 apply modus_ponens.
 normalize. apply exp_right with z.
 apply andp_left1. apply andp_left1.
 rewrite lseg_eq. apply derives_trans with (next x z * emp).
  rewrite sepcon_emp; auto. apply sepcon_derives; auto.
 apply now_later.
Qed.

 Lemma allp_andp1 {A}{NA: NatDed A}{B}: forall (any: B) (P: B -> A) Q,
   allp P && Q = ALL x:B, P x && Q.
Proof. intros. apply pred_ext. apply allp_right; intro x.
   apply andp_derives; auto. apply allp_left with x; auto.
   apply andp_right. apply allp_right; intro x; apply allp_left with x.
  apply andp_left1; auto. apply allp_left with any. apply andp_left2; auto.
Qed.

Lemma list_append:  (* U3 *)
   forall x y, lseg x y * lseg y 0 |-- lseg x 0.
Proof.
 intros.
  generalize (loeb (ALL x:adr, lseg x y * lseg y 0  >=> lseg x 0)) ; intro.
 apply subp_e.
  eapply derives_trans; [ apply H; clear H | apply allp_left with x; auto].
  apply allp_right; intro z.
  apply subp_i1.
  match goal with |- ! |> ?S' && _ |-- _ => remember S' as S end.
  rewrite (lseg_unfold z y).
  rewrite distrib_orp_sepcon.
  rewrite andp_comm.
  rewrite distrib_orp_andp.
  apply orp_left; normalize.
  apply derives_trans with (next z tail * |> (lseg tail y * lseg y 0) && !|>S).
  apply andp_derives; auto.
  rewrite sepcon_assoc; apply sepcon_derives; auto.
  rewrite later_sepcon; apply sepcon_derives; auto. apply now_later.
  rewrite (lseg_unfold z 0). apply orp_right1.
  apply andp_right.
  unfold next. normalize. apply prop_right. omega.
  apply exp_right with tail.
  rewrite andp_comm; rewrite unfash_sepcon_distrib.
  apply sepcon_derives. apply andp_left2; auto.
  rewrite <- later_unfash; rewrite <- later_andp; apply later_derives.
  subst. rewrite unfash_allp.
 rewrite allp_andp1; [ | apply 0].
 apply allp_left with tail.
 rewrite andp_comm.
 eapply derives_trans; [ eapply andp_derives; [ apply derives_refl | apply unfash_fash] | ].
 apply modus_ponens.
  apply andp_left1; auto.
Qed.

Lemma lseg_U5:
    forall x y z w, z<>w -> lseg x y * next y z * lseg z w |-- lseg x z * lseg z w.
Proof.
 intros.
 rewrite (lseg_neq z w); auto.
 repeat rewrite exp_sepcon2.
 normalize. intro v. apply exp_right with v.
 repeat rewrite <- sepcon_assoc.
 apply sepcon_derives; auto.
 apply lseg_cons_in_next_context.
Qed.

Lemma lseg_cons_in_list_context:
    forall x y z, lseg x y * next y z * lseg z 0 |-- lseg x z * lseg z 0.
Proof.
  intros.
  destruct (eq_dec z 0).
  subst. rewrite lseg_eq. repeat  rewrite sepcon_emp.
  eapply derives_trans; try apply list_append.
  apply sepcon_derives; eauto.
  rewrite next_gt_0. normalize.
  apply next_lseg; omega.
  apply lseg_U5; auto.
Qed.

author: PrincetonUniversity

repo: VST


text:
Require Import list_examples.

Require Import ZArith.
Require Import List.

(*

struct listNode* append(struct listNode *x, struct listNode *y)
/*@ rule <k> $ => return ?x; ...</k>
         <heap>... list(x)(A), list(y)(B) => list(?x)(A @ B) ...</heap> */
{
  struct listNode *p;
  if (x == NULL)
    return y;

  p = x;
  /*@ inv <heap>... lseg(x, p)(?A1), list(p)(?A2) ...</heap>
          /\ A = ?A1 @ ?A2 /\ ~(p = 0) */
  while (p->next != NULL)
    p = p->next;
  p->next = y;

  return x;
}

//@ var A, B : Seq
*)

Open Scope Z.

Definition append_loop :=
  (SWhile (ELoad ("p" + 1) <> 0)
      ("p" <- ELoad ("p"+1)))%code.
Definition append_tail :=
 {{"p"+1 <<- "y"
  ;SReturn "x"
  }}%code.
Definition append_code :=
  SIf ("x"=0)
    (SReturn (EVar "y"))
    (Seq ("p" <- "x")
    (Seq append_loop
         append_tail))%code.

Inductive append_spec : kcfg -> (kcfg -> Prop) -> Prop :=
  append_claim : forall c,
    kcell c = kra (KStmt append_code) kdot ->
    forall xv yv pv, store c ~= "x" s|-> KInt xv :* "y" s|-> KInt yv :* "p" s|-> KInt pv ->
    forall lx ly m, heap c |= rep_list lx xv :* rep_list ly yv :* litP m ->
      append_spec c (returns_list c (lx ++ ly) m)
 |loop_claim : forall c,
    kcell c = kra (KStmt append_loop) (kra (KStmt append_tail) kdot) ->
    forall xv yv pv, store c ~= "x" s|-> KInt xv :* "y" s|-> KInt yv :* "p" s|-> KInt pv ->
    pv <> 0%Z ->
    forall lx lp ly m, heap c |= rep_seg lx pv xv :* rep_list lp pv :* rep_list ly yv :* litP m ->
      append_spec c (returns_list c (lx ++ lp ++ ly) m).

Lemma append_proof : sound kstep append_spec.
list_solver.
rewrite app_ass in * |-.
list_run.
Qed.

author: Formal-Systems-Laboratory

repo: coinduction


text:
From Hammer Require Import Hammer.

Require Export Finite_sets.
Require Export Constructive_sets.
Require Export Classical.
Require Export Classical_sets.
Require Export Powerset.
Require Export Powerset_facts.
Require Export Powerset_Classical_facts.
Require Export Gt.
Require Export Lt.

Section Finite_sets_facts.
Variable U : Type.

Lemma finite_cardinal :
forall X:Ensemble U, Finite U X ->  exists n : nat, cardinal U X n.
Proof. hammer_hook "Finite_sets_facts" "Finite_sets_facts.finite_cardinal".
induction 1 as [| A _ [n H]].
exists 0; auto with sets.
exists (S n); auto with sets.
Qed.

Lemma cardinal_finite :
forall (X:Ensemble U) (n:nat), cardinal U X n -> Finite U X.
Proof. hammer_hook "Finite_sets_facts" "Finite_sets_facts.cardinal_finite".
induction 1; auto with sets.
Qed.

Theorem Add_preserves_Finite :
forall (X:Ensemble U) (x:U), Finite U X -> Finite U (Add U X x).
Proof. hammer_hook "Finite_sets_facts" "Finite_sets_facts.Add_preserves_Finite".
intros X x H'.
elim (classic (In U X x)); intro H'0; auto with sets.
rewrite (Non_disjoint_union U X x); auto with sets.
Qed.

Theorem Singleton_is_finite : forall x:U, Finite U (Singleton U x).
Proof. hammer_hook "Finite_sets_facts" "Finite_sets_facts.Singleton_is_finite".
intro x; rewrite <- (Empty_set_zero U (Singleton U x)).
change (Finite U (Add U (Empty_set U) x)); auto with sets.
Qed.

Theorem Union_preserves_Finite :
forall X Y:Ensemble U, Finite U X -> Finite U Y -> Finite U (Union U X Y).
Proof. hammer_hook "Finite_sets_facts" "Finite_sets_facts.Union_preserves_Finite".
intros X Y H; induction H as [|A Fin_A Hind x].
rewrite (Empty_set_zero U Y). trivial.
intros.
rewrite (Union_commutative U (Add U A x) Y).
rewrite <- (Union_add U Y A x).
rewrite (Union_commutative U Y A).
apply Add_preserves_Finite.
apply Hind. assumption.
Qed.

Lemma Finite_downward_closed :
forall A:Ensemble U,
Finite U A -> forall X:Ensemble U, Included U X A -> Finite U X.
Proof. hammer_hook "Finite_sets_facts" "Finite_sets_facts.Finite_downward_closed".
intros A H'; elim H'; auto with sets.
intros X H'0.
rewrite (less_than_empty U X H'0); auto with sets.
intros; elim Included_Add with U X A0 x; auto with sets.
destruct 1 as [A' [H5 H6]].
rewrite H5; auto with sets.
Qed.

Lemma Intersection_preserves_finite :
forall A:Ensemble U,
Finite U A -> forall X:Ensemble U, Finite U (Intersection U X A).
Proof. hammer_hook "Finite_sets_facts" "Finite_sets_facts.Intersection_preserves_finite".
intros A H' X; apply Finite_downward_closed with A; auto with sets.
Qed.

Lemma cardinalO_empty :
forall X:Ensemble U, cardinal U X 0 -> X = Empty_set U.
Proof. hammer_hook "Finite_sets_facts" "Finite_sets_facts.cardinalO_empty".
intros X H; apply (cardinal_invert U X 0); trivial with sets.
Qed.

Lemma inh_card_gt_O :
forall X:Ensemble U, Inhabited U X -> forall n:nat, cardinal U X n -> n > 0.
Proof. hammer_hook "Finite_sets_facts" "Finite_sets_facts.inh_card_gt_O".
induction 1 as [x H'].
intros n H'0.
elim (gt_O_eq n); auto with sets.
intro H'1; generalize H'; generalize H'0.
rewrite <- H'1; intro H'2.
rewrite (cardinalO_empty X); auto with sets.
intro H'3; elim H'3.
Qed.

Lemma card_soustr_1 :
forall (X:Ensemble U) (n:nat),
cardinal U X n ->
forall x:U, In U X x -> cardinal U (Subtract U X x) (pred n).
Proof. hammer_hook "Finite_sets_facts" "Finite_sets_facts.card_soustr_1".
intros X n H'; elim H'.
intros x H'0; elim H'0.
clear H' n X.
intros X n H' H'0 x H'1 x0 H'2.
elim (classic (In U X x0)).
intro H'4; rewrite (add_soustr_xy U X x x0).
elim (classic (x = x0)).
intro H'5.
absurd (In U X x0); auto with sets.
rewrite <- H'5; auto with sets.
intro H'3; try assumption.
cut (S (pred n) = pred (S n)).
intro H'5; rewrite <- H'5.
apply card_add; auto with sets.
red; intro H'6; elim H'6.
intros H'7 H'8; try assumption.
elim H'1; auto with sets.
unfold pred at 2; symmetry .
apply S_pred with (m := 0).
change (n > 0).
apply inh_card_gt_O with (X := X); auto with sets.
apply Inhabited_intro with (x := x0); auto with sets.
red; intro H'3.
apply H'1.
elim H'3; auto with sets.
rewrite H'3; auto with sets.
elim (classic (x = x0)).
intro H'3; rewrite <- H'3.
cut (Subtract U (Add U X x) x = X); auto with sets.
intro H'4; rewrite H'4; auto with sets.
intros H'3 H'4; try assumption.
absurd (In U (Add U X x) x0); auto with sets.
red; intro H'5; try exact H'5.
lapply (Add_inv U X x x0); tauto.
Qed.

Lemma cardinal_is_functional :
forall (X:Ensemble U) (c1:nat),
cardinal U X c1 ->
forall (Y:Ensemble U) (c2:nat), cardinal U Y c2 -> X = Y -> c1 = c2.
Proof. hammer_hook "Finite_sets_facts" "Finite_sets_facts.cardinal_is_functional".
intros X c1 H'; elim H'.
intros Y c2 H'0; elim H'0; auto with sets.
intros A n H'1 H'2 x H'3 H'5.
elim (not_Empty_Add U A x); auto with sets.
clear H' c1 X.
intros X n H' H'0 x H'1 Y c2 H'2.
elim H'2.
intro H'3.
elim (not_Empty_Add U X x); auto with sets.
clear H'2 c2 Y.
intros X0 c2 H'2 H'3 x0 H'4 H'5.
elim (classic (In U X0 x)).
intro H'6; apply f_equal.
apply H'0 with (Y := Subtract U (Add U X0 x0) x).
elimtype (pred (S c2) = c2); auto with sets.
apply card_soustr_1; auto with sets.
rewrite <- H'5.
apply Sub_Add_new; auto with sets.
elim (classic (x = x0)).
intros H'6 H'7; apply f_equal.
apply H'0 with (Y := X0); auto with sets.
apply Simplify_add with (x := x); auto with sets.
pattern x at 2; rewrite H'6; auto with sets.
intros H'6 H'7.
absurd (Add U X x = Add U X0 x0); auto with sets.
clear H'0 H' H'3 n H'5 H'4 H'2 H'1 c2.
red; intro H'.
lapply (Extension U (Add U X x) (Add U X0 x0)); auto with sets.
clear H'.
intro H'; red in H'.
elim H'; intros H'0 H'1; red in H'0; clear H' H'1.
absurd (In U (Add U X0 x0) x); auto with sets.
lapply (Add_inv U X0 x0 x); [ intuition | apply (H'0 x); apply Add_intro2 ].
Qed.

Lemma cardinal_Empty : forall m:nat, cardinal U (Empty_set U) m -> 0 = m.
Proof. hammer_hook "Finite_sets_facts" "Finite_sets_facts.cardinal_Empty".
intros m Cm; generalize (cardinal_invert U (Empty_set U) m Cm).
elim m; auto with sets.
intros; elim H0; intros; elim H1; intros; elim H2; intros.
elim (not_Empty_Add U x x0 H3).
Qed.

Lemma cardinal_unicity :
forall (X:Ensemble U) (n:nat),
cardinal U X n -> forall m:nat, cardinal U X m -> n = m.
Proof. hammer_hook "Finite_sets_facts" "Finite_sets_facts.cardinal_unicity".
intros; apply cardinal_is_functional with X X; auto with sets.
Qed.

Lemma card_Add_gen :
forall (A:Ensemble U) (x:U) (n n':nat),
cardinal U A n -> cardinal U (Add U A x) n' -> n' <= S n.
Proof. hammer_hook "Finite_sets_facts" "Finite_sets_facts.card_Add_gen".
intros A x n n' H'.
elim (classic (In U A x)).
intro H'0.
rewrite (Non_disjoint_union U A x H'0).
intro H'1; cut (n = n').
intro E; rewrite E; auto with sets.
apply cardinal_unicity with A; auto with sets.
intros H'0 H'1.
cut (n' = S n).
intro E; rewrite E; auto with sets.
apply cardinal_unicity with (Add U A x); auto with sets.
Qed.

Lemma incl_st_card_lt :
forall (X:Ensemble U) (c1:nat),
cardinal U X c1 ->
forall (Y:Ensemble U) (c2:nat),
cardinal U Y c2 -> Strict_Included U X Y -> c2 > c1.
Proof. hammer_hook "Finite_sets_facts" "Finite_sets_facts.incl_st_card_lt".
intros X c1 H'; elim H'.
intros Y c2 H'0; elim H'0; auto with sets arith.
intro H'1.
elim (Strict_Included_strict U (Empty_set U)); auto with sets arith.
clear H' c1 X.
intros X n H' H'0 x H'1 Y c2 H'2.
elim H'2.
intro H'3; elim (not_SIncl_empty U (Add U X x)); auto with sets arith.
clear H'2 c2 Y.
intros X0 c2 H'2 H'3 x0 H'4 H'5; elim (classic (In U X0 x)).
intro H'6; apply gt_n_S.
apply H'0 with (Y := Subtract U (Add U X0 x0) x).
elimtype (pred (S c2) = c2); auto with sets arith.
apply card_soustr_1; auto with sets arith.
apply incl_st_add_soustr; auto with sets arith.
elim (classic (x = x0)).
intros H'6 H'7; apply gt_n_S.
apply H'0 with (Y := X0); auto with sets arith.
apply sincl_add_x with (x := x0).
rewrite <- H'6; auto with sets arith.
pattern x0 at 1; rewrite <- H'6; trivial with sets arith.
intros H'6 H'7; red in H'5.
elim H'5; intros H'8 H'9; try exact H'8; clear H'5.
red in H'8.
generalize (H'8 x).
intro H'5; lapply H'5; auto with sets arith.
intro H; elim Add_inv with U X0 x0 x; auto with sets arith.
intro; absurd (In U X0 x); auto with sets arith.
intro; absurd (x = x0); auto with sets arith.
Qed.

Lemma incl_card_le :
forall (X Y:Ensemble U) (n m:nat),
cardinal U X n -> cardinal U Y m -> Included U X Y -> n <= m.
Proof. hammer_hook "Finite_sets_facts" "Finite_sets_facts.incl_card_le".
intros; elim Included_Strict_Included with U X Y; auto with sets arith; intro.
cut (m > n); auto with sets arith.
apply incl_st_card_lt with (X := X) (Y := Y); auto with sets arith.
generalize H0; rewrite <- H2; intro.
cut (n = m).
intro E; rewrite E; auto with sets arith.
apply cardinal_unicity with X; auto with sets arith.
Qed.

Lemma G_aux :
forall P:Ensemble U -> Prop,
(forall X:Ensemble U,
Finite U X ->
(forall Y:Ensemble U, Strict_Included U Y X -> P Y) -> P X) ->
P (Empty_set U).
Proof. hammer_hook "Finite_sets_facts" "Finite_sets_facts.G_aux".
intros P H'; try assumption.
apply H'; auto with sets.
clear H'; auto with sets.
intros Y H'; try assumption.
red in H'.
elim H'; intros H'0 H'1; try exact H'1; clear H'.
lapply (less_than_empty U Y); [ intro H'3; try exact H'3 | assumption ].
elim H'1; auto with sets.
Qed.

Lemma Generalized_induction_on_finite_sets :
forall P:Ensemble U -> Prop,
(forall X:Ensemble U,
Finite U X ->
(forall Y:Ensemble U, Strict_Included U Y X -> P Y) -> P X) ->
forall X:Ensemble U, Finite U X -> P X.
Proof. hammer_hook "Finite_sets_facts" "Finite_sets_facts.Generalized_induction_on_finite_sets".
intros P H'0 X H'1.
generalize P H'0; clear H'0 P.
elim H'1.
intros P H'0.
apply G_aux; auto with sets.
clear H'1 X.
intros A H' H'0 x H'1 P H'3.
cut (forall Y:Ensemble U, Included U Y (Add U A x) -> P Y); auto with sets.
generalize H'1.
apply H'0.
intros X K H'5 L Y H'6; apply H'3; auto with sets.
apply Finite_downward_closed with (A := Add U X x); auto with sets.
intros Y0 H'7.
elim (Strict_inclusion_is_transitive_with_inclusion U Y0 Y (Add U X x));
auto with sets.
intros H'2 H'4.
elim (Included_Add U Y0 X x);
[ intro H'14
| intro H'14; elim H'14; intros A' E; elim E; intros H'15 H'16; clear E H'14
| idtac ]; auto with sets.
elim (Included_Strict_Included U Y0 X); auto with sets.
intro H'9; apply H'5 with (Y := Y0); auto with sets.
intro H'9; rewrite H'9.
apply H'3; auto with sets.
intros Y1 H'8; elim H'8.
intros H'10 H'11; apply H'5 with (Y := Y1); auto with sets.
elim (Included_Strict_Included U A' X); auto with sets.
intro H'8; apply H'5 with (Y := A'); auto with sets.
rewrite <- H'15; auto with sets.
intro H'8.
elim H'7.
intros H'9 H'10; apply H'10 || elim H'10; try assumption.
generalize H'6.
rewrite <- H'8.
rewrite <- H'15; auto with sets.
Qed.

End Finite_sets_facts.

author: lukaszcz

repo: coqhammer-eval