Require Import VST.floyd.base2.
Require Import VST.floyd.client_lemmas.

Local Open Scope logic.

Lemma canon1: forall P1 B  P Q R,
   do_canon (prop P1 && B) (PROPx P (LOCALx Q (SEPx R))) = do_canon B  (PROPx (P1::P) (LOCALx Q (SEPx R))).
Proof.
(* Goal: forall (R1 : lift_T (LiftEnviron mpred)) (P : list Prop) (Q : list localdef) (R : list mpred), @eq (forall _ : environ, mpred) (do_canon (@liftx (LiftEnviron mpred) (R1 : lift_T (LiftEnviron mpred))) (PROPx P (LOCALx Q (SEPx R)))) (PROPx P (LOCALx Q (SEPx (@cons (lift_T (LiftEnviron mpred)) R1 R)))) *)
unfold do_canon, PROPx, LOCALx, SEPx; intros.
(* Goal: @eq (forall _ : environ, mpred) (fun x : environ => @andp mpred Nveric (local (locald_denote Q1) x) (@andp mpred Nveric (@prop mpred Nveric (@fold_right Prop Prop and True P)) (@andp mpred Nveric (local (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q)) x) (R x)))) (fun x : environ => @andp mpred Nveric (@prop mpred Nveric (@fold_right Prop Prop and True P)) (@andp mpred Nveric (local (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (locald_denote Q1) (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) x) (R x))) *)
extensionality rho.
(* Goal: @eq mpred (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@liftx (LiftEnviron mpred) R1) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@fold_right Prop Prop and True P)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (@fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) (fun _ : environ => fold_right_sepcon R))) rho) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@fold_right Prop Prop and True P)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (@fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) (fun _ : environ => fold_right_sepcon (@cons (lift_T (LiftEnviron mpred)) R1 R))) rho) *)
simpl.
(* Goal: @eq mpred (@andp mpred Nveric (local (locald_denote Q1) rho) (@andp mpred Nveric (@prop mpred Nveric (@fold_right Prop Prop and True P)) (@andp mpred Nveric (local (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q)) rho) (R rho)))) (@andp mpred Nveric (@prop mpred Nveric (@fold_right Prop Prop and True P)) (@andp mpred Nveric (local (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (locald_denote Q1) (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) rho) (R rho))) *)
normalize.
Qed.

Lemma canon2: forall Q1 B P Q R,
    do_canon (local (locald_denote Q1) && B) (PROPx P (LOCALx Q (SEPx R))) = do_canon B (PROPx (P) (LOCALx (Q1::Q) (SEPx R))).
Proof.
(* Goal: forall (R1 : lift_T (LiftEnviron mpred)) (P : list Prop) (Q : list localdef) (R : list mpred), @eq (forall _ : environ, mpred) (do_canon (@liftx (LiftEnviron mpred) (R1 : lift_T (LiftEnviron mpred))) (PROPx P (LOCALx Q (SEPx R)))) (PROPx P (LOCALx Q (SEPx (@cons (lift_T (LiftEnviron mpred)) R1 R)))) *)
unfold do_canon, PROPx, LOCALx, SEPx; intros.
(* Goal: @eq (forall _ : environ, mpred) (fun x : environ => @andp mpred Nveric (local (locald_denote Q1) x) (@andp mpred Nveric (@prop mpred Nveric (@fold_right Prop Prop and True P)) (@andp mpred Nveric (local (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q)) x) (R x)))) (fun x : environ => @andp mpred Nveric (@prop mpred Nveric (@fold_right Prop Prop and True P)) (@andp mpred Nveric (local (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (locald_denote Q1) (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) x) (R x))) *)
extensionality rho.
(* Goal: @eq mpred (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@liftx (LiftEnviron mpred) R1) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@fold_right Prop Prop and True P)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (@fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) (fun _ : environ => fold_right_sepcon R))) rho) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@fold_right Prop Prop and True P)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (@fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) (fun _ : environ => fold_right_sepcon (@cons (lift_T (LiftEnviron mpred)) R1 R))) rho) *)
simpl.
(* Goal: @eq mpred (@andp mpred Nveric (local (locald_denote Q1) rho) (@andp mpred Nveric (@prop mpred Nveric (@fold_right Prop Prop and True P)) (@andp mpred Nveric (local (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q)) rho) (R rho)))) (@andp mpred Nveric (@prop mpred Nveric (@fold_right Prop Prop and True P)) (@andp mpred Nveric (local (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (locald_denote Q1) (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) rho) (R rho))) *)
normalize. autorewrite with norm1 norm2; normalize.
Qed.

Definition nonlocal (Q: environ->mpred) := True.

Ltac check_nonlocal :=
  match goal with
  |  |- nonlocal (local _) => fail 1
  |  |- nonlocal (prop _) => fail 1
  |  |- nonlocal (andp _ _) => fail 1
  |  |- nonlocal (sepcon _ _) => fail 1
  | |- _ => apply I
 end.

Lemma canon3: forall R1 B P Q R,
    nonlocal `(R1) ->
    do_canon (B * `(R1)) (PROPx P (LOCALx Q (SEPx R))) = do_canon B (PROPx (P) (LOCALx Q (SEPx (R1::R)))).
Proof.
(* Goal: forall (R1 : lift_T (LiftEnviron mpred)) (P : list Prop) (Q : list localdef) (R : list mpred), @eq (forall _ : environ, mpred) (do_canon (@liftx (LiftEnviron mpred) (R1 : lift_T (LiftEnviron mpred))) (PROPx P (LOCALx Q (SEPx R)))) (PROPx P (LOCALx Q (SEPx (@cons (lift_T (LiftEnviron mpred)) R1 R)))) *)
unfold do_canon, PROPx, LOCALx, SEPx; intros.
(* Goal: @eq (forall _ : environ, mpred) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@sepcon (lifted (LiftEnviron mpred)) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) B (@liftx (LiftEnviron mpred) R1)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@fold_right Prop Prop and True P)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (@fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) (fun _ : environ => fold_right_sepcon R)))) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) B (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@fold_right Prop Prop and True P)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (@fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) (fun _ : environ => fold_right_sepcon (@cons (lift_T (LiftEnviron mpred)) R1 R))))) *)
clear H.
(* Goal: @eq (forall _ : environ, mpred) (fun x : environ => @andp mpred Nveric (local (locald_denote Q1) x) (@andp mpred Nveric (@prop mpred Nveric (@fold_right Prop Prop and True P)) (@andp mpred Nveric (local (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q)) x) (R x)))) (fun x : environ => @andp mpred Nveric (@prop mpred Nveric (@fold_right Prop Prop and True P)) (@andp mpred Nveric (local (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (locald_denote Q1) (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) x) (R x))) *)
extensionality rho.
(* Goal: @eq mpred (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@liftx (LiftEnviron mpred) R1) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@fold_right Prop Prop and True P)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (@fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) (fun _ : environ => fold_right_sepcon R))) rho) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@fold_right Prop Prop and True P)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (@fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) (fun _ : environ => fold_right_sepcon (@cons (lift_T (LiftEnviron mpred)) R1 R))) rho) *)
simpl.
(* Goal: @eq mpred (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (B rho) (@liftx (LiftEnviron mpred) R1 rho)) (@andp mpred Nveric (@prop mpred Nveric (@fold_right Prop Prop and True P)) (@andp mpred Nveric (local (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q)) rho) (fold_right_sepcon R)))) (@sepcon mpred Nveric Sveric (B rho) (@andp mpred Nveric (@prop mpred Nveric (@fold_right Prop Prop and True P)) (@andp mpred Nveric (local (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q)) rho) (@sepcon mpred Nveric Sveric R1 (fold_right_sepcon R))))) *)
rewrite sepcon_assoc.
(* Goal: @eq (forall _ : environ, mpred) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local R) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) S Q)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local R) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q S)) *)
f_equal.
(* Goal: @eq mpred (@sepcon mpred Nveric Sveric (@liftx (LiftEnviron mpred) R1 rho) (@andp mpred Nveric (@prop mpred Nveric (@fold_right Prop Prop and True P)) (@andp mpred Nveric (local (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q)) rho) (fold_right_sepcon R)))) (@andp mpred Nveric (@prop mpred Nveric (@fold_right Prop Prop and True P)) (@andp mpred Nveric (local (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q)) rho) (@sepcon mpred Nveric Sveric R1 (fold_right_sepcon R)))) *)
rewrite sepcon_andp_prop.
(* Goal: @eq (forall _ : environ, mpred) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local R) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) S Q)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local R) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q S)) *)
f_equal.
(* Goal: @eq mpred (@andp mpred Nveric (local (locald_denote Q1) rho) (@andp mpred Nveric (@prop mpred Nveric (@fold_right Prop Prop and True P)) (@andp mpred Nveric (local (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q)) rho) (R rho)))) (@andp mpred Nveric (@prop mpred Nveric (@fold_right Prop Prop and True P)) (@andp mpred Nveric (local (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (locald_denote Q1) (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) rho) (R rho))) *)
normalize. autorewrite with norm1 norm2; normalize.
Qed.

Lemma canon3b: forall R1 B P Q R,
    nonlocal `(R1) ->
    do_canon (`(R1)* B) (PROPx P (LOCALx Q (SEPx R))) = do_canon B (PROPx (P) (LOCALx Q (SEPx (R1::R)))).
Proof.
(* Goal: forall (R1 : lift_T (LiftEnviron mpred)) (P : list Prop) (Q : list localdef) (R : list mpred), @eq (forall _ : environ, mpred) (do_canon (@liftx (LiftEnviron mpred) (R1 : lift_T (LiftEnviron mpred))) (PROPx P (LOCALx Q (SEPx R)))) (PROPx P (LOCALx Q (SEPx (@cons (lift_T (LiftEnviron mpred)) R1 R)))) *)
unfold do_canon, PROPx, LOCALx, SEPx; intros.
(* Goal: @eq (forall _ : environ, mpred) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@sepcon (lifted (LiftEnviron mpred)) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@liftx (LiftEnviron mpred) R1) B) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@fold_right Prop Prop and True P)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (@fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) (fun _ : environ => fold_right_sepcon R)))) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) B (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@fold_right Prop Prop and True P)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (@fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) (fun _ : environ => fold_right_sepcon (@cons (lift_T (LiftEnviron mpred)) R1 R))))) *)
rewrite (sepcon_comm `(R1) B).
(* Goal: @eq (forall _ : environ, mpred) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@sepcon (lifted (LiftEnviron mpred)) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) B (@liftx (LiftEnviron mpred) R1)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@fold_right Prop Prop and True P)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (@fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) (fun _ : environ => fold_right_sepcon R)))) (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) B (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@fold_right Prop Prop and True P)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (@fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) (fun _ : environ => fold_right_sepcon (@cons (lift_T (LiftEnviron mpred)) R1 R))))) *)
apply canon3. auto.
Qed.

Lemma canon4: forall P, do_canon emp P = P.
Proof.
(* Goal: forall P : forall _ : environ, mpred, @eq (forall _ : environ, mpred) (do_canon (@emp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric)) P) P *)
apply emp_sepcon.
Qed.

Lemma canon7: forall R1 P Q R,
   nonlocal `(R1) ->
   do_canon `(R1) (PROPx P (LOCALx Q (SEPx R))) = (PROPx P (LOCALx Q (SEPx (R1::R)))).
Proof.
(* Goal: forall (R1 : lift_T (LiftEnviron mpred)) (P : list Prop) (Q : list localdef) (R : list mpred), @eq (forall _ : environ, mpred) (do_canon (@liftx (LiftEnviron mpred) (R1 : lift_T (LiftEnviron mpred))) (PROPx P (LOCALx Q (SEPx R)))) (PROPx P (LOCALx Q (SEPx (@cons (lift_T (LiftEnviron mpred)) R1 R)))) *)
unfold do_canon, PROPx, LOCALx, SEPx; intros.
(* Goal: @eq (forall _ : environ, mpred) (fun x : environ => @andp mpred Nveric (local (locald_denote Q1) x) (@andp mpred Nveric (@prop mpred Nveric (@fold_right Prop Prop and True P)) (@andp mpred Nveric (local (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q)) x) (R x)))) (fun x : environ => @andp mpred Nveric (@prop mpred Nveric (@fold_right Prop Prop and True P)) (@andp mpred Nveric (local (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (locald_denote Q1) (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) x) (R x))) *)
extensionality rho.
(* Goal: @eq mpred (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@liftx (LiftEnviron mpred) R1) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@fold_right Prop Prop and True P)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (@fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) (fun _ : environ => fold_right_sepcon R))) rho) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@fold_right Prop Prop and True P)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (@fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) (fun _ : environ => fold_right_sepcon (@cons (lift_T (LiftEnviron mpred)) R1 R))) rho) *)
simpl.
(* Goal: @eq mpred (@andp mpred Nveric (local (locald_denote Q1) rho) (@andp mpred Nveric (@prop mpred Nveric (@fold_right Prop Prop and True P)) (@andp mpred Nveric (local (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q)) rho) (R rho)))) (@andp mpred Nveric (@prop mpred Nveric (@fold_right Prop Prop and True P)) (@andp mpred Nveric (local (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (locald_denote Q1) (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) rho) (R rho))) *)
normalize. autorewrite with norm1 norm2; normalize.
Qed.

Lemma canon8: forall R1 R2 R3 PQR,
    do_canon ((R1 && R2) && R3) PQR = do_canon (R1 && (R2 && R3)) PQR.
(* Goal: @eq (forall _ : environ, mpred) (PROPx P (LOCALx Q (SEPx R))) (PROPx P (LOCALx Q (SEPx R))) *)
Proof. intros; rewrite andp_assoc; auto.
Qed.

Lemma start_canon: forall P, P  = do_canon P (PROPx nil (LOCALx nil (SEPx nil ))).
Proof.
(* Goal: forall (R1 : lift_T (LiftEnviron mpred)) (P : list Prop) (Q : list localdef) (R : list mpred), @eq (forall _ : environ, mpred) (do_canon (@liftx (LiftEnviron mpred) (R1 : lift_T (LiftEnviron mpred))) (PROPx P (LOCALx Q (SEPx R)))) (PROPx P (LOCALx Q (SEPx (@cons (lift_T (LiftEnviron mpred)) R1 R)))) *)
unfold do_canon, PROPx, LOCALx, SEPx; intros.
(* Goal: @eq mpred (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@liftx (LiftEnviron mpred) R1) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@fold_right Prop Prop and True P)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (@fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) (fun _ : environ => fold_right_sepcon R))) rho) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@fold_right Prop Prop and True P)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (@fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) (fun _ : environ => fold_right_sepcon (@cons (lift_T (LiftEnviron mpred)) R1 R))) rho) *)
extensionality rho; simpl.
(* Goal: @eq mpred (@andp mpred Nveric (local (locald_denote Q1) rho) (@andp mpred Nveric (@prop mpred Nveric (@fold_right Prop Prop and True P)) (@andp mpred Nveric (local (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q)) rho) (R rho)))) (@andp mpred Nveric (@prop mpred Nveric (@fold_right Prop Prop and True P)) (@andp mpred Nveric (local (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (locald_denote Q1) (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) rho) (R rho))) *)
normalize.
Qed.

Hint Rewrite canon1 canon2 canon4 canon8 : canon.
Hint Rewrite canon3 using check_nonlocal : canon.
Hint Rewrite canon3b using check_nonlocal : canon.
Hint Rewrite canon7 using check_nonlocal : canon.
Hint Rewrite <- (@sepcon_assoc (environ->mpred) _) : canon.

Lemma canon5: forall Q R S,
       nonlocal Q ->
       Q && (local R && S) = local R && (Q && S).
Proof.
(* Goal: forall (P : list Prop) (Q : list localdef) (R : list mpred), @eq (forall _ : environ, mpred) (PROPx P (LOCALx Q (SEPx R))) (do_canon (@emp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric)) (PROPx P (LOCALx Q (SEPx R)))) *)
intros.
(* Goal: @eq (forall _ : environ, mpred) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local R) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) S Q)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local R) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q S)) *)
rewrite andp_comm. rewrite andp_assoc. f_equal. apply andp_comm.
Qed.

Lemma canon5b: forall Q R S,
       nonlocal Q ->
       Q && (S && local R) = local R && (Q && S).
Proof.
(* Goal: forall (P : list Prop) (Q : list localdef) (R : list mpred), @eq (forall _ : environ, mpred) (PROPx P (LOCALx Q (SEPx R))) (do_canon (@emp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric)) (PROPx P (LOCALx Q (SEPx R)))) *)
intros.
(* Goal: @eq (forall _ : environ, mpred) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) S (local R))) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local R) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q S)) *)
symmetry.
(* Goal: @eq (forall _ : environ, mpred) (PROPx P (LOCALx Q (SEPx R))) (PROPx P (LOCALx Q (SEPx R))) *)
rewrite andp_comm. rewrite andp_assoc. auto.
Qed.

Lemma canon5c: forall Q R,
       nonlocal Q ->
       (Q && local R) = local R && Q.
Proof.
(* Goal: forall (P : list Prop) (Q : list localdef) (R : list mpred), @eq (forall _ : environ, mpred) (PROPx P (LOCALx Q (SEPx R))) (do_canon (@emp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric)) (PROPx P (LOCALx Q (SEPx R)))) *)
intros.
(* Goal: @eq (forall _ : environ, mpred) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) R)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) R) Q) *)
apply andp_comm.
Qed.

Lemma canon6: forall Q R S,
       nonlocal Q ->
       Q && (prop R && S) = prop R && (Q && S).
Proof.
(* Goal: forall (P : list Prop) (Q : list localdef) (R : list mpred), @eq (forall _ : environ, mpred) (PROPx P (LOCALx Q (SEPx R))) (do_canon (@emp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric)) (PROPx P (LOCALx Q (SEPx R)))) *)
intros.
(* Goal: @eq (forall _ : environ, mpred) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local R) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) S Q)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local R) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q S)) *)
rewrite andp_comm. rewrite andp_assoc; f_equal. apply andp_comm.
Qed.

Lemma canon6b: forall Q R S,
       nonlocal Q ->
       Q && (S && prop R) = prop R && (Q && S).
Proof.
(* Goal: forall (P : list Prop) (Q : list localdef) (R : list mpred), @eq (forall _ : environ, mpred) (PROPx P (LOCALx Q (SEPx R))) (do_canon (@emp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric)) (PROPx P (LOCALx Q (SEPx R)))) *)
intros.
(* Goal: @eq (forall _ : environ, mpred) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local R) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) S Q)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local R) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q S)) *)
   symmetry; rewrite andp_comm. rewrite andp_assoc; f_equal.
Qed.

Lemma canon6c: forall Q R,
       nonlocal Q ->
       (Q && prop R) = prop R && Q.
Proof.
(* Goal: forall (P : list Prop) (Q : list localdef) (R : list mpred), @eq (forall _ : environ, mpred) (PROPx P (LOCALx Q (SEPx R))) (do_canon (@emp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric)) (PROPx P (LOCALx Q (SEPx R)))) *)
intros.
(* Goal: @eq (forall _ : environ, mpred) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Q (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) R)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) R) Q) *)
 apply andp_comm.
Qed.

Hint Rewrite canon5 using check_nonlocal : canon.
Hint Rewrite canon5b using check_nonlocal : canon.
Hint Rewrite canon5c using check_nonlocal : canon.
Hint Rewrite canon6 using check_nonlocal : canon.
Hint Rewrite canon6b using check_nonlocal : canon.
Hint Rewrite canon6c using check_nonlocal : canon.

Lemma canon17 : forall (P: Prop) PP QR, prop P && (PROPx PP QR) = PROPx (P::PP) QR.
Proof.
(* Goal: @eq (forall _ : environ, mpred) (fun x : environ => @andp mpred Nveric (local (locald_denote Q1) x) (@andp mpred Nveric (@prop mpred Nveric (@fold_right Prop Prop and True P)) (@andp mpred Nveric (local (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q)) x) (R x)))) (fun x : environ => @andp mpred Nveric (@prop mpred Nveric (@fold_right Prop Prop and True P)) (@andp mpred Nveric (local (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (locald_denote Q1) (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) x) (R x))) *)
intros. unfold PROPx. simpl. extensionality rho. apply pred_ext; normalize.
Qed.
Hint Rewrite canon17 : canon.


Lemma finish_canon: forall R1 P Q R,
   do_canon `(R1) (PROPx P (LOCALx Q (SEPx R))) = (PROPx P (LOCALx Q (SEPx (R1::R)))).
Proof.
(* Goal: forall (R1 : lift_T (LiftEnviron mpred)) (P : list Prop) (Q : list localdef) (R : list mpred), @eq (forall _ : environ, mpred) (do_canon (@liftx (LiftEnviron mpred) (R1 : lift_T (LiftEnviron mpred))) (PROPx P (LOCALx Q (SEPx R)))) (PROPx P (LOCALx Q (SEPx (@cons (lift_T (LiftEnviron mpred)) R1 R)))) *)
unfold do_canon, PROPx, LOCALx, SEPx; intros.
(* Goal: @eq (forall _ : environ, mpred) (fun x : environ => @andp mpred Nveric (local (locald_denote Q1) x) (@andp mpred Nveric (@prop mpred Nveric (@fold_right Prop Prop and True P)) (@andp mpred Nveric (local (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q)) x) (R x)))) (fun x : environ => @andp mpred Nveric (@prop mpred Nveric (@fold_right Prop Prop and True P)) (@andp mpred Nveric (local (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (locald_denote Q1) (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) x) (R x))) *)
extensionality rho.
(* Goal: @eq mpred (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@liftx (LiftEnviron mpred) R1) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@fold_right Prop Prop and True P)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (@fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) (fun _ : environ => fold_right_sepcon R))) rho) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@fold_right Prop Prop and True P)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (@fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) (fun _ : environ => fold_right_sepcon (@cons (lift_T (LiftEnviron mpred)) R1 R))) rho) *)
simpl.
(* Goal: @eq mpred (@andp mpred Nveric (local (locald_denote Q1) rho) (@andp mpred Nveric (@prop mpred Nveric (@fold_right Prop Prop and True P)) (@andp mpred Nveric (local (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q)) rho) (R rho)))) (@andp mpred Nveric (@prop mpred Nveric (@fold_right Prop Prop and True P)) (@andp mpred Nveric (local (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (locald_denote Q1) (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) rho) (R rho))) *)
normalize. autorewrite with norm1 norm2; normalize.
Qed.

Ltac canonicalize_pre :=
  match goal with |- semax _ ?P _ _ =>
      rewrite (start_canon P); autorewrite with canon
  end.

Lemma restart_canon: forall P Q R, (PROPx P (LOCALx Q (SEPx R))) = do_canon emp (PROPx P (LOCALx Q (SEPx R))).
Proof.
(* Goal: forall (P : list Prop) (Q : list localdef) (R : list mpred), @eq (forall _ : environ, mpred) (PROPx P (LOCALx Q (SEPx R))) (do_canon (@emp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric)) (PROPx P (LOCALx Q (SEPx R)))) *)
intros.
(* Goal: @eq (forall _ : environ, mpred) (PROPx P (LOCALx Q (SEPx R))) (PROPx P (LOCALx Q (SEPx R))) *)
unfold do_canon. rewrite emp_sepcon. auto.
Qed.

Lemma exp_do_canon:
   forall T (P: T -> environ->mpred) (Q: environ->mpred), do_canon (exp P) Q = EX x:_, do_canon (P x) Q.
Proof. apply exp_sepcon1. Qed.
Hint Rewrite exp_do_canon: canon.
Hint Rewrite exp_do_canon: norm2.

Lemma canon9: forall Q1 P Q R,
       local (locald_denote Q1) && (PROPx P (LOCALx Q R)) =
         PROPx P (LOCALx (Q1::Q) R).
Proof.
(* Goal: @eq mpred (@sepcon (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric) (@liftx (LiftEnviron mpred) R1) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@fold_right Prop Prop and True P)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (@fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) (fun _ : environ => fold_right_sepcon R))) rho) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@fold_right Prop Prop and True P)) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (@fold_right (forall _ : lift_S (LiftEnviron Prop), Prop) (forall _ : lift_S (Tarrow Prop (LiftEnviron Prop)), Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) (fun _ : environ => fold_right_sepcon (@cons (lift_T (LiftEnviron mpred)) R1 R))) rho) *)
intros; unfold PROPx, LOCALx; simpl.
(* Goal: @eq (forall _ : environ, mpred) (fun x : environ => @andp mpred Nveric (local (locald_denote Q1) x) (@andp mpred Nveric (@prop mpred Nveric (@fold_right Prop Prop and True P)) (@andp mpred Nveric (local (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q)) x) (R x)))) (fun x : environ => @andp mpred Nveric (@prop mpred Nveric (@fold_right Prop Prop and True P)) (@andp mpred Nveric (local (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (locald_denote Q1) (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) x) (R x))) *)
extensionality rho.
(* Goal: @eq mpred (@andp mpred Nveric (local (locald_denote Q1) rho) (@andp mpred Nveric (@prop mpred Nveric (@fold_right Prop Prop and True P)) (@andp mpred Nveric (local (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q)) rho) (R rho)))) (@andp mpred Nveric (@prop mpred Nveric (@fold_right Prop Prop and True P)) (@andp mpred Nveric (local (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (locald_denote Q1) (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) rho) (R rho))) *)
normalize.
(* Goal: @eq mpred (@andp mpred Nveric (local (locald_denote Q1) rho) (@andp mpred Nveric (@prop mpred Nveric (@fold_right Prop Prop and True P)) (@andp mpred Nveric (local (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q)) rho) (R rho)))) (@andp mpred Nveric (@prop mpred Nveric (@fold_right Prop Prop and True P)) (@andp mpred Nveric (local (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and (locald_denote Q1) (@fold_right (forall _ : environ, Prop) (forall _ : environ, Prop) (@liftx (Tarrow Prop (Tarrow Prop (LiftEnviron Prop))) and) (@liftx (LiftEnviron Prop) True) (@map localdef (forall _ : environ, Prop) locald_denote Q))) rho) (R rho))) *)
apply pred_ext; normalize; autorewrite with norm1 norm2; normalize.
Qed.
Hint Rewrite canon9: canon.


Lemma canon20: forall PQR, do_canon emp PQR = PQR.
Proof.
(* Goal: forall P : forall _ : environ, mpred, @eq (forall _ : environ, mpred) (do_canon (@emp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@LiftSepLog' mpred Nveric Sveric)) P) P *)
intros. apply emp_sepcon.
Qed.
Hint Rewrite canon20: canon.

