(** Heavily annotated for a tutorial introduction. *)

(** First, import the entire Floyd proof automation system, which includes
 ** the VeriC program logic and the MSL theory of separation logic**)
Require Import VST.floyd.proofauto.

(** Import the [reverse.v] file, which is produced by CompCert's clightgen
 ** from reverse.c.   The file reverse.v defines abbreviations for identifiers
 ** (variable names, etc.) of the C program, such as _head, _reverse.
 ** It also defines "prog", which is the entire abstract syntax tree
 ** of the C program *)
Require Import VST.progs.reverse.

(* The C programming language has a special namespace for struct
** and union identifiers, e.g., "struct foo {...}".  Some type-based operators
** in the program logic need access to an interpretation of this namespace,
** i.e., the meaning of each struct-identifier such as "foo".  The next
** line (which looks identical for any program) builds this
** interpretation, called "CompSpecs" *)
Instance CompSpecs : compspecs. make_compspecs prog. Defined.

(** Calculate the "types-of-global-variables" specification
 ** directly from the program *)
Definition Vprog : varspecs. mk_varspecs prog. Defined.

(** A convenience definition *)
Definition t_struct_list := Tstruct _list noattr.

(** Inductive definition of linked lists *)
Fixpoint listrep (sigma: list val) (x: val) : mpred :=
 match sigma with
 | h::hs => 
    EX y:val, 
      data_at Tsh t_struct_list (h,y) x  *  listrep hs y
 | nil => 
    !! (x = nullval) && emp
 end.

Fixpoint lsegrec (sigma: list val) (x z: val) : mpred :=
 match sigma with
 | h::hs => 
    EX y:val, 
      data_at Tsh t_struct_list (h,y) x  *  lsegrec hs y z
 | nil => 
    !! (x = z) && emp
 end.

(* This file is only to demonstrate object language induction. *)

(* induction rule *)

Lemma list_ind_in_logc: forall {A: Type} (P: mpred) (Q: list A -> mpred),
  P |-- Q nil ->
  P |-- ALL a: A, (ALL l: list A, Q l --> Q (a :: l)) ->
  P |-- ALL l: list A, Q l.
Proof.
(* Goal: forall (l : list val) (x : val), @derives mpred Nveric (listrep l x) (lsegrec l x nullval) *)
  intros.
(* Goal: @derives mpred Nveric P (@allp mpred Nveric (list A) (fun l : list A => Q l)) *)
  apply allp_right; intro l.
(* Goal: @derives mpred Nveric P (Q l) *)
  induction l; auto.
(* Goal: @derives mpred Nveric P (Q (@cons A a l)) *)
  rewrite (add_andp _ _ IHl), (add_andp _ _ H0).
(* Goal: @derives mpred Nveric (@emp mpred Nveric Sveric) (@imp mpred Nveric (@allp mpred Nveric val (fun x : val => @wand mpred Nveric Sveric (listrep l x) (lsegrec l x nullval))) (@allp mpred Nveric val (fun x : val => @wand mpred Nveric Sveric (listrep (@cons val a l) x) (lsegrec (@cons val a l) x nullval)))) *)
  apply imp_andp_adjoint.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@emp mpred Nveric Sveric) (@allp mpred Nveric val (fun x : val => @wand mpred Nveric Sveric (listrep l x) (lsegrec l x nullval)))) (@wand mpred Nveric Sveric (listrep (@cons val a l) x) (lsegrec (@cons val a l) x nullval)) *)
  apply andp_left2.
(* Goal: @derives mpred Nveric (@allp mpred Nveric A (fun a : A => @allp mpred Nveric (list A) (fun l : list A => @imp mpred Nveric (Q l) (Q (@cons A a l))))) (@imp mpred Nveric (Q l) (Q (@cons A a l))) *)
  apply (allp_left _ a).
(* Goal: @derives mpred Nveric (@allp mpred Nveric (list val) (fun l : list val => @allp mpred Nveric val (fun x : val => @wand mpred Nveric Sveric (listrep l x) (lsegrec l x nullval)))) (@wand mpred Nveric Sveric (listrep l x) (lsegrec l x nullval)) *)
  apply (allp_left _ l).
(* Goal: @derives mpred Nveric (@imp mpred Nveric (Q l) (Q (@cons A a l))) (@imp mpred Nveric (Q l) (Q (@cons A a l))) *)
  auto.
Qed.

(* application *)

Lemma listrep2lsegrec: forall l x,
  listrep l x |-- lsegrec l x nullval.
Proof.
(* Goal: forall (l : list val) (x : val), @derives mpred Nveric (listrep l x) (lsegrec l x nullval) *)
  assert (emp |-- ALL l: list val, (ALL x: val, listrep l x -* lsegrec l x nullval)).
  + apply list_ind_in_logc.
(* Goal: forall (l : list val) (x : val), @derives mpred Nveric (listrep l x) (lsegrec l x nullval) *)
    - apply allp_right; intros.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@emp mpred Nveric Sveric) (listrep l x)) (lsegrec l x nullval) *)
      apply wand_sepcon_adjoint.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@emp mpred Nveric Sveric) (listrep (@nil val) v)) (lsegrec (@nil val) v nullval) *)
      rewrite emp_sepcon.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@allp mpred Nveric val (fun x : val => @wand mpred Nveric Sveric (listrep l x) (lsegrec l x nullval))) (listrep (@cons val a l) x)) (lsegrec (@cons val a l) x nullval) *)
      simpl.
(* Goal: @derives mpred Nveric (@wand mpred Nveric Sveric (listrep l x) (lsegrec l x nullval)) (@wand mpred Nveric Sveric (listrep l x) (lsegrec l x nullval)) *)
      apply derives_refl.
    - apply allp_right; intros a.
(* Goal: @derives mpred Nveric (@emp mpred Nveric Sveric) (@allp mpred Nveric (list val) (fun l : list val => @imp mpred Nveric (@allp mpred Nveric val (fun x : val => @wand mpred Nveric Sveric (listrep l x) (lsegrec l x nullval))) (@allp mpred Nveric val (fun x : val => @wand mpred Nveric Sveric (listrep (@cons val a l) x) (lsegrec (@cons val a l) x nullval))))) *)
      apply allp_right; intros l.
(* Goal: @derives mpred Nveric (@emp mpred Nveric Sveric) (@imp mpred Nveric (@allp mpred Nveric val (fun x : val => @wand mpred Nveric Sveric (listrep l x) (lsegrec l x nullval))) (@allp mpred Nveric val (fun x : val => @wand mpred Nveric Sveric (listrep (@cons val a l) x) (lsegrec (@cons val a l) x nullval)))) *)
      apply imp_andp_adjoint.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@emp mpred Nveric Sveric) (@allp mpred Nveric val (fun x : val => @wand mpred Nveric Sveric (listrep l x) (lsegrec l x nullval)))) (@allp mpred Nveric val (fun x : val => @wand mpred Nveric Sveric (listrep (@cons val a l) x) (lsegrec (@cons val a l) x nullval))) *)
      apply allp_right; intros x.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@emp mpred Nveric Sveric) (@allp mpred Nveric val (fun x : val => @wand mpred Nveric Sveric (listrep l x) (lsegrec l x nullval)))) (@wand mpred Nveric Sveric (listrep (@cons val a l) x) (lsegrec (@cons val a l) x nullval)) *)
      apply andp_left2.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@emp mpred Nveric Sveric) (listrep l x)) (lsegrec l x nullval) *)
      apply wand_sepcon_adjoint.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@allp mpred Nveric val (fun x : val => @wand mpred Nveric Sveric (listrep l x) (lsegrec l x nullval))) (listrep (@cons val a l) x)) (lsegrec (@cons val a l) x nullval) *)
      simpl.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@allp mpred Nveric val (fun x : val => @wand mpred Nveric Sveric (listrep l x) (lsegrec l x nullval))) (@exp mpred Nveric val (fun y : val => @sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh t_struct_list (@pair val val a y) x) (listrep l y)))) (@exp mpred Nveric val (fun y : val => @sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh t_struct_list (@pair val val a y) x) (lsegrec l y nullval))) *)
      Intros y.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@allp mpred Nveric val (fun x : val => @wand mpred Nveric Sveric (listrep l x) (lsegrec l x nullval))) (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh t_struct_list (@pair val val a y) x) (listrep l y))) (@exp mpred Nveric val (fun y : val => @sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh t_struct_list (@pair val val a y) x) (lsegrec l y nullval))) *)
      Exists y.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@emp mpred Nveric Sveric) (listrep l x)) (lsegrec l x nullval) *)
      apply wand_sepcon_adjoint.
(* Goal: @derives mpred Nveric (@allp mpred Nveric val (fun x : val => @wand mpred Nveric Sveric (listrep l x) (lsegrec l x nullval))) (@wand mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh t_struct_list (@pair val val a y) x) (listrep l y)) (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh t_struct_list (@pair val val a y) x) (lsegrec l y nullval))) *)
      apply (allp_left _ y).
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@emp mpred Nveric Sveric) (listrep l x)) (lsegrec l x nullval) *)
      apply wand_sepcon_adjoint.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@wand mpred Nveric Sveric (listrep l y) (lsegrec l y nullval)) (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh t_struct_list (@pair val val a y) x) (listrep l y))) (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh t_struct_list (@pair val val a y) x) (lsegrec l y nullval)) *)
      cancel.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@emp mpred Nveric Sveric) (listrep l x)) (lsegrec l x nullval) *)
      apply wand_sepcon_adjoint.
(* Goal: @derives mpred Nveric (@wand mpred Nveric Sveric (listrep l x) (lsegrec l x nullval)) (@wand mpred Nveric Sveric (listrep l x) (lsegrec l x nullval)) *)
      apply derives_refl.
(* Goal: forall (l : list val) (x : val), @derives mpred Nveric (listrep l x) (lsegrec l x nullval) *)
  + intros.
    rewrite <- (emp_sepcon (listrep _ _)).
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@emp mpred Nveric Sveric) (listrep l x)) (lsegrec l x nullval) *)
    apply wand_sepcon_adjoint.
(* Goal: @derives mpred Nveric (@emp mpred Nveric Sveric) (@wand mpred Nveric Sveric (listrep l x) (lsegrec l x nullval)) *)
    eapply derives_trans; [exact H | clear H].
(* Goal: @derives mpred Nveric (@allp mpred Nveric (list val) (fun l : list val => @allp mpred Nveric val (fun x : val => @wand mpred Nveric Sveric (listrep l x) (lsegrec l x nullval)))) (@wand mpred Nveric Sveric (listrep l x) (lsegrec l x nullval)) *)
    apply (allp_left _ l).
(* Goal: @derives mpred Nveric (@allp mpred Nveric val (fun x : val => @wand mpred Nveric Sveric (listrep l x) (lsegrec l x nullval))) (@wand mpred Nveric Sveric (listrep l x) (lsegrec l x nullval)) *)
    apply (allp_left _ x).
(* Goal: @derives mpred Nveric (@wand mpred Nveric Sveric (listrep l x) (lsegrec l x nullval)) (@wand mpred Nveric Sveric (listrep l x) (lsegrec l x nullval)) *)
    apply derives_refl.
Qed.
