text:
(* --------------------------------------------------------------------
 * Copyright (c) - 2006--2012 - IMDEA Software Institute
 * Copyright (c) - 2006--2012 - Inria
 * Copyright (c) - 2006--2012 - Microsoft Coprporation
 *
 * Distributed under the terms of the CeCILL-B-V1 license
 * -------------------------------------------------------------------- *)

(** * SemTheory,v : Properties about the denotational semantics of programs and
  general theory of program equivalence *)

Set Implicit Arguments.

Require Export BaseProp.

Module Make (Sem:SEM).

 Module BP := BaseProp.Make Sem.
 Export BP.

 Lemma equiv_refl : forall E c,
  equiv Mem.eq E c E c Mem.eq.
 Proof.
  intros E c k.
  exists (fun m1 m2 => Mlet ([[c]] E m2) (fun m => Munit (m,m))).
  constructor; simpl; intros.
  apply Mem.eq_leibniz in H; rewrite H.
  refine (mu_stable_eq _ _ _ _); refine (ford_eq_intro _); intro m; trivial.
  refine (mu_stable_eq _ _ _ _); refine (ford_eq_intro _); intro m; trivial.
  intros f Hf; simpl.
  rewrite <- (mu_0 ([[c]] E m2)).
  apply mu_stable_eq; refine (ford_eq_intro _); intro m; apply Hf.
  unfold Mem.eq, prodP; auto.
 Qed.

 Lemma equiv_strengthen : forall (P P' Q:mem_rel) E1 c1 E2 c2,
  (forall k (m1 m2:Mem.t k), P' k m1 m2 -> P k m1 m2) ->
  equiv P  E1 c1 E2 c2 Q ->
  equiv P' E1 c1 E2 c2 Q.
 Proof.
  unfold equiv; intros.
  destruct (H0 k) as (d,Hd); exists d; intros; auto.
 Qed.

 Lemma equiv_weaken : forall (P Q Q':mem_rel) E1 c1 E2 c2,
  (forall k (m1 m2:Mem.t k), Q k m1 m2 -> Q' k m1 m2) ->
  equiv P E1 c1 E2 c2 Q ->
  equiv P E1 c1 E2 c2 Q'.
 Proof.
  unfold equiv; intros.
  destruct (H0 k) as (d,Hd); exists d; intros.
  apply lift_weaken with (Q k); auto.
 Qed.

 Lemma equiv_sub : forall (P P' Q Q':mem_rel) E1 c1 E2 c2,
  (forall k (m1 m2:Mem.t k), P' k m1 m2 -> P k m1 m2) ->
  (forall k (m1 m2:Mem.t k), Q k m1 m2 -> Q' k m1 m2) ->
  equiv P  E1 c1 E2 c2 Q ->
  equiv P' E1 c1 E2 c2 Q'.
 Proof.
  intros.
  apply equiv_strengthen with P; [ | apply equiv_weaken with Q]; trivial.
 Qed.

 Add Morphism equiv
  with signature implMR ++> (@eq env) ==> (@eq cmd) ==>
   (@eq env) ==> (@eq cmd) ==> implMR --> inverse impl
  as equiv_imp_Morph.
 Proof.
  unfold flip, implMR, impl; intros P P' H ? ? ? ? Q Q' ? ?.
  eapply equiv_sub with P' Q'; auto.
 Qed.

 Add Morphism equiv
  with signature iffMR ==> (@eq env) ==> (@eq cmd) ==>
   (@eq env) ==> (@eq cmd) ==> iffMR ==> iff
  as equiv_iff_Morph.
 Proof.
  unfold iffMR; intros.
  destruct H; destruct H0; split; intros.
  rewrite <- H0, H1; trivial.
  rewrite <- H2, H; trivial.
 Qed.

 Lemma equiv_sym_transp : forall (P Q:mem_rel) E1 c1 E2 c2,
  equiv (transpR P) E1 c1 E2 c2 (transpR Q) ->
  equiv P E2 c2 E1 c1 Q.
 Proof.
  unfold equiv; intros.
  destruct (H k) as (d,Hd).
  exists (fun m1 m2 => Mlet (d m2 m1) (fun p => Munit (snd p, fst p))).
  intros; apply lift_weaken with (transp _ (transp _ (Q k))).
  intros x y H1; exact H1.
  apply lift_sym.
  apply Hd.
  red; trivial.
 Qed.

 Lemma equiv_sym : forall (P Q:mem_rel) E1 c1 E2 c2,
  symMR P -> symMR Q ->
  equiv P E1 c1 E2 c2 Q ->
  equiv P E2 c2 E1 c1 Q.
 Proof.
  unfold symMR; intros; apply equiv_sym_transp.
  rewrite H, H0; trivial.
 Qed.

 Lemma equiv_trans : forall (P1 P2 Q1 Q2 Q3:mem_rel) E1 c1 E2 c2 E3 c3,
  decMR P2 ->
  refl_supMR2 P2 P1 ->
  (forall k x y z, Q1 k x y -> Q2 k y z -> Q3 k x z) ->
  equiv P1 E1 c1 E2 c2 Q1 ->
  equiv P2 E2 c2 E3 c3 Q2 ->
  equiv P2 E1 c1 E3 c3 Q3.
 Proof.
  intros.
  intros k; destruct (H1 k) as (d, Hd); destruct (H2 k) as (d',Hd').
  exists (
   fun m1 m3 =>
    match X k m1 m3 with
    | left HP2 =>
       let HP1 := H _ _ _ HP2 in
        dd' (@mem_eqU k) (Hd _ _ HP1) (Hd' _ _ HP2)
    | _ => distr0 _
    end).
  intros m1 m3 HP2.
  destruct (X k m1 m3); simpl.
  apply lift_trans_discr; auto using mem_eqU_spec.
  exact (H0 k).
  apply sem_discr.
  elim n; trivial.
 Qed.

 Lemma equiv_trans_r : forall (P1 P2 Q1 Q2 Q3:mem_rel) E1 c1 E2 c2 E3 c3,
  decMR P1 ->
  refl_supMR2 (transpR P1) (transpR P2) ->
  (forall k x y z, Q1 k x y -> Q2 k y z -> Q3 k x z) ->
  equiv P1 E1 c1 E2 c2 Q1 ->
  equiv P2 E2 c2 E3 c3 Q2 ->
  equiv P1 E1 c1 E3 c3 Q3.
 Proof.
  intros; apply equiv_sym_transp.
  apply equiv_trans with (P1 := transpR P2) (P2:=transpR P1)
   (Q1 := transpR Q2) (Q2 := transpR Q1) (E2 := E2) (c2:= c2).
  auto.
  trivial.
  unfold transpR; intros; eapply H0; eauto.
  apply equiv_sym_transp; repeat rewrite transpR_transpR; trivial.
  apply equiv_sym_transp; repeat rewrite transpR_transpR; trivial.
 Qed.

 Lemma equiv_trans_trial : forall (P1 P2 P3 Q1 Q2 Q3:mem_rel) E1 c1 E2 c2 E3 c3,
  decMR P3 ->
  (forall k x z, P3 k x z -> sigS (fun y  =>  P1 k x y /\ P2 k y z)) ->
  (forall k x y z, Q1 k x y -> Q2 k y z -> Q3 k x z) ->
  equiv P1 E1 c1 E2 c2 Q1 ->
  equiv P2 E2 c2 E3 c3 Q2 ->
  equiv P3 E1 c1 E3 c3 Q3.
 Proof.
  intros.
  intros k; destruct (H0 k) as (d, Hd); destruct (H1 k) as (d',Hd').
  exists (
   fun m1 m3 =>
    match X k m1 m3 with
    | left HP3 =>
       let (m2, HH) := X0 k m1 m3 HP3 in
       let (HP1, HP2) := HH in
       dd' (@mem_eqU k) (Hd _ _ HP1) (Hd' _ _ HP2)
    | _ => distr0 _
    end).
  intros m1 m3 HP3.
  destruct (X k m1 m3); simpl.
  destruct (X0 k m1 m3) as (m2, (HP1, HP2)).
  apply lift_trans_discr; auto using mem_eqU_spec.
  exact (H k).
  apply sem_discr.
  elim n; trivial.
 Qed.

 Lemma equiv_trans_trans : forall P Q E1 c1 E2 c2 E3 c3,
   decMR P ->
   refl_supMR P ->
   transMR Q ->
   equiv P E1 c1 E2 c2 Q ->
   equiv P E2 c2 E3 c3 Q ->
   equiv P E1 c1 E3 c3 Q.
 Proof.
  intros; eapply equiv_trans; eauto; trivial.
 Qed.

 (* Used for optimizations *)
 Lemma equiv_trans_eq_mem_l : forall P1 P Q E1 c1 E1' c1' E2 c2,
  equiv (Meq /-\ P1) E1 c1 E1' c1' Meq ->
  equiv P E1' c1' E2 c2 Q ->
  refl_supMR2 P P1 ->
  equiv P E1 c1 E2 c2 Q.
 Proof.
  unfold equiv, implMR; intros.
  destruct (H k) as (d, Hd); destruct (H0 k) as (d',Hd').
  exists d'; intros.
  eapply lift_eq_trans_l with (d:=d m1 m1); auto.
  apply lift_weaken with (Meq k).
  unfold Meq; trivial.
  apply Hd ; red; split; eauto.
 Qed.

 Lemma equiv_trans_eq_mem_r : forall P2 P Q E1 c1 E2 c2 E2' c2',
  equiv (Meq /-\ P2) E2 c2 E2' c2' Meq ->
  equiv P E1 c1 E2' c2' Q ->
  refl_supMR2 (transpR P) P2 ->
  equiv P E1 c1 E2 c2 Q.
 Proof.
  intros; apply equiv_sym_transp.
  apply equiv_trans_eq_mem_l with P2 E2' c2'; trivial.
  apply equiv_sym_transp; simplMR; trivial.
 Qed.

 Lemma equiv_depend_only_l : forall (P:mem_rel) E1 c1 E1' c1' E2 c2 (Q:mem_rel) X1 X2,
  decMR P ->
  depend_only_rel Q X1 X2 ->
  equiv Meq E1 c1 E1' c1' (kreq_mem X1) ->
  equiv P E1' c1' E2 c2 Q ->
  equiv P E1 c1 E2 c2 Q.
 Proof.
  intros; apply equiv_trans with (P1:= Meq) (Q1:= kreq_mem X1) (Q2 := Q)
    (E2:= E1') (c2:= c1'); auto.
  red; red; trivial.
  unfold kreq_mem; intros k x y z H2 H3; apply H with (3:= H3); auto.
 Qed.

 Lemma equiv_depend_only_r : forall (P:mem_rel) E1 c1 E2 c2 E2' c2' Q X1 X2,
  decMR P ->
  depend_only_rel Q X1 X2 ->
  equiv Meq E2 c2 E2' c2' (kreq_mem X2) ->
  equiv P E1 c1 E2' c2' Q ->
  equiv P E1 c1 E2 c2 Q.
 Proof.
  intros; apply equiv_sym_transp.
  eapply equiv_depend_only_l with (X2:= X1); eauto.
  apply equiv_sym_transp; simplMR; trivial.
 Qed.

 Lemma equiv_True : forall P E1 c1 E2 c2,
  lossless E1 c1 ->
  lossless E2 c2 ->
  equiv P E1 c1 E2 c2 trueR.
 Proof.
  unfold lossless, equiv; intros P E1 c1 E2 c2 Hc1 Hc2 k.
  exists (fun m1 m2 => prod_distr ([[c1]] E1 m1) ([[c2]] E2 m2)); intros.
  constructor; simpl; intros.
  apply (mu_stable_eq ([[c1]] E1 m1)); simpl; apply ford_eq_intro; intros.
  change (fun _ :Mem.t k=> f n) with (fcte (Mem.t k) (f n)).
  rewrite (mu_cte ([[c2]] E2 m2) (f n)).
  unfold fone; rewrite Hc2; auto.
  change (
   mu (([[c1]]) E1 m1) (fcte (Mem.t k) (mu (([[c2]]) E2 m2) (fun (x0 : Mem.t k) => f x0))) ==
   mu (([[c2]]) E2 m2) f).
  rewrite  (mu_cte ([[c1]] E1 m1)).
  unfold fone; rewrite Hc1;Usimpl.
  apply (mu_stable_eq ([[c2]]E2 m2)); simpl; apply ford_eq_intro; trivial.
  unfold prodP; apply range_True.
 Qed.

 Lemma equiv_falseR : forall E E' Q c c',
  equiv falseR E c E' c' Q.
 Proof.
  unfold equiv; intros.
  exists (fun m1 m2 => distr0 _).
  unfold falseR; tauto.
 Qed.

 Hint Resolve equiv_falseR.

 Lemma equiv_False : forall (P:mem_rel) E1 c1 E2 c2 Q,
  (forall k m1 m2, P k m1 m2 -> False) ->
  equiv P E1 c1 E2 c2 Q.
 Proof.
  intros; apply equiv_strengthen with falseR.
  unfold falseR; trivial.
  apply equiv_falseR.
 Qed.

 Lemma equiv_case1 : forall (A P Q:mem_rel) E1 c1 E2 c2,
  (forall k x y, sumbool (A k x y) (~A k x y)) ->
  equiv (P /-\ A) E1 c1 E2 c2 Q ->
  equiv (P /-\ ~- A) E1 c1 E2 c2 Q ->
  equiv P E1 c1 E2 c2 Q.
 Proof.
  unfold andR, notR; intros A P Q E1 c1 E2 c2 H H0 H1 k.
  destruct (H0 k) as (d,Hd); destruct (H1 k) as (d',Hd').
  exists (fun m1 m2 => if H k m1 m2 then d m1 m2 else d' m1 m2); intros.
  destruct (H k m1 m2); auto.
 Qed.

 Lemma equiv_case2 : forall (A P Q:mem_rel) E1 c1 E2 c2,
  (forall k x y,sumbool (P k x y) (~P k x y)) ->
  (forall k x y, P k x y -> sumbool (A k x y) (~A k x y)) ->
  equiv (P /-\ A) E1 c1 E2 c2 Q ->
  equiv (P /-\ ~- A) E1 c1 E2 c2 Q ->
  equiv P E1 c1 E2 c2 Q.
 Proof.
  unfold andR, notR; intros A P Q E1 c1 E2 c2 H H0 H1 H2 k.
  destruct (H1 k) as (d,Hd); destruct (H2 k) as (d',Hd').
  exists (fun m1 m2 =>
    match H k m1 m2 with
    | left H1 => if (H0 k m1 m2 H1) then d m1 m2 else d' m1 m2
    | _ => distr0 _
    end); intros.
  destruct (H k m1 m2); intros.
  destruct (H0 k m1 m2 p); auto.
  elim n; trivial.
 Qed.

 Lemma equiv_eq_sem_pre : forall E1 E2 c1 c2 (P:mem_rel),
  (forall k (m:Mem.t k), P k m m -> [[c1]] E1 m == [[c2]] E2 m) ->
  equiv (Meq /-\ P ) E1 c1 E2 c2 Meq.
 Proof.
  unfold equiv; intros.
  exists (fun m1 m2 => Mlet ([[c1]] E1 m1) (fun x => Munit (x, x))).
  unfold Meq, andR; intros m1 m2 (H1, H2); subst.
  apply lift_weaken with (@eq (Mem.t k)); auto.
  rewrite (H _ _ H2).
  apply lift_eq_refl.
 Qed.

 Lemma equiv_eq_sem : forall E1 c1 E2 c2,
  (forall k (m:Mem.t k), [[c1]] E1 m == [[c2]] E2 m) ->
  equiv Meq E1 c1 E2 c2 Meq.
 Proof.
  intros; apply equiv_strengthen with (Meq /-\ trueR).
  unfold andR, trueR; tauto.
  apply equiv_eq_sem_pre; auto.
 Qed.

 Lemma equiv_eq_mem : forall E c, equiv Meq E c E c Meq.
 Proof.
  intros; apply equiv_eq_sem; trivial.
 Qed.

 Lemma equiv_nil : forall P E1 E2, equiv P E1 nil E2 nil P.
 Proof.
  unfold equiv; intros.
  exists (fun m1 m2 => Munit (m1, m2)); intros.
  repeat rewrite deno_nil; apply lift_unit; trivial.
 Qed.

 Lemma equiv_nil_impl : forall P E1 E2 Q,
  implMR P Q -> equiv P E1 nil E2 nil Q.
 Proof.
  intros P E1 E2 Q H; rewrite H; apply equiv_nil.
 Qed.

 Lemma equiv_app : forall P Q R E c1 c2 E' c3 c4,
  equiv P E c1 E' c3 Q ->
  equiv Q E c2 E' c4 R ->
  equiv P E (c1++c2) E' (c3++c4) R.
 Proof.
  unfold equiv; intros.
  destruct (H k) as (d, Hd); destruct (H0 k) as (d', Hd').
  exists (fun m1 m2 => Mlet (d m1 m2) (fun p => d' (fst p) (snd p))); intros.
  repeat rewrite deno_app; apply lift_Mlet with (Q k); auto.
 Qed.

 Lemma equiv_cons : forall P Q R E1 i1 c1 E2 i2 c2,
  equiv P E1 [i1] E2 [i2] Q ->
  equiv Q E1 c1 E2 c2 R ->
  equiv P E1 (i1::c1) E2 (i2::c2) R.
 Proof.
  intros P Q R E1 i1 c1 E2 i2 c2  H H0.
  apply equiv_app with (Q:=Q) (c1:=[i1]) (c2:=c1) (c3:=[i2]) (c4:=c2); trivial.
 Qed.

 Lemma equiv_cond_l : forall P E1 e c c' E2 c2 Q,
  equiv (P /-\ EP1 e) E1 c E2 c2 Q ->
  equiv (P /-\ ~- EP1 e) E1 c' E2 c2 Q ->
  equiv P E1 [If e then c else c'] E2 c2 Q.
 Proof.
  unfold equiv, andR, notR,EP1,is_true.
  intros P E3 e1 c c' E4 c2 Q HD HD' k.
  destruct (HD k) as (d3,Hd); destruct (HD' k) as (d',Hd').
  exists (fun m1 m2 =>
   if E.eval_expr e1 m1 then d3 m1 m2  else d' m1 m2); intros.
  case_eq (E.eval_expr e1 m1); intros Heq;
   rewrite deno_cond; rewrite Heq;[apply Hd | apply Hd']; split; autob.
 Qed.

 Lemma equiv_cond_r :  forall P E1 c1 E2 e c c' Q,
  equiv (P /-\ EP2 e) E1 c1 E2 c Q ->
  equiv (P /-\ ~- EP2 e) E1 c1 E2 c' Q ->
  equiv P E1 c1 E2 [If e then c else c'] Q.
 Proof.
  intros; apply equiv_sym_transp.
  apply equiv_cond_l; apply equiv_sym_transp; simplMR; trivial.
 Qed.

 Lemma equiv_cond : forall P Q E1 (e1:E.expr T.Bool) c1 c2 E2 (e2:E.expr T.Bool) c3 c4,
  equiv (P /-\ (EP1 e1 /-\ EP2 e2)) E1 c1 E2 c3 Q ->
  equiv (P /-\ (~- EP1 e1 /-\ ~- EP2 e2)) E1 c2 E2 c4 Q ->
  (forall k m1 m2, P k m1 m2 -> E.eval_expr e1 m1 = E.eval_expr e2 m2) ->
  equiv P E1 [If e1 then c1 else c2] E2 [If e2 then c3 else c4] Q.
 Proof.
  intros; apply equiv_cond_l; apply equiv_cond_r.
  simplMR; trivial.
  apply equiv_False; unfold andR,notR,EP1,EP2.
  intros k m1 m2 ((H2, H3), H4); apply H4; erewrite <- H1; eauto.
  apply equiv_False; unfold andR,notR,EP1,EP2.
  intros k m1 m2 ((H2, H3), H4); apply H3; erewrite H1; eauto.
  simplMR; trivial.
 Qed.

 Lemma equiv_while : forall (P:mem_rel) E1 (e1:E.expr T.Bool) c1 E2 (e2:E.expr T.Bool) c2,
  (forall k m1 m2, P k m1 m2 -> E.eval_expr e1 m1 = E.eval_expr e2 m2) ->
  equiv (P /-\ EP1 e1 /-\ EP2 e2) E1 c1 E2 c2 P ->
  equiv P E1 [while e1 do c1] E2 [while e2 do c2] (P /-\ ~-EP1 e1 /-\ ~-EP2 e2).
 Proof.
  unfold equiv,andR,notR,EP1, EP2, is_true; intros.
  destruct (H0 k) as (d, Hd).
  assert  (forall (m1 m2 : Mem.t k),
   P k m1 m2 ->
   E.eval_expr e1 m1 = true ->
   lift (P k) (d m1 m2) (([[c1]]) E1 m1) (([[c2]]) E2 m2)).
  intros; apply Hd.
  rewrite <- (H _ _ _ H1); auto.
  destruct (while_indR d _ _ (H k) H1) as (d', Hd').
  exists d'; intros.
  apply lift_weaken with (2:= Hd' _ _ H2).
  intros x y (H4,H3); rewrite <- (H _ _ _ H4); rewrite H3; auto.
 Qed.

 Lemma equiv_assign_l : forall Q E1 E2 t1 (x1:Var.var t1) e1,
  equiv (upd1 Q x1 e1) E1 [x1 <- e1] E2 nil Q.
 Proof.
  unfold equiv; intros.
  exists (fun m1 m2 => Munit (m1{!x1<--E.eval_expr e1 m1!}, m2)); intros.
  rewrite deno_assign; rewrite deno_nil; auto using lift_unit.
 Qed.

 Lemma equiv_assign_r : forall Q E1 E2 t2 (x2:Var.var t2) e2,
  equiv (upd2 Q x2 e2) E1 nil E2 [x2 <- e2] Q.
 Proof.
  unfold equiv; intros.
  exists (fun m1 m2 => Munit (m1, m2{!x2<--E.eval_expr e2 m2!})); intros.
  rewrite deno_assign; rewrite deno_nil; auto using lift_unit.
 Qed.

 Lemma equiv_assign : forall Q E1 E2 t1 (x1:Var.var t1) t2 (x2:Var.var t2) e1 e2,
   equiv (upd_para Q x1 e1 x2 e2) E1 [x1 <- e1] E2 [x2 <- e2] Q.
 Proof.
  unfold equiv; intros.
  exists (fun m1 m2 => Munit (m1{!x1<-- E.eval_expr e1 m1!}, m2{!x2<--E.eval_expr e2 m2!})); intros.
  repeat rewrite deno_assign; auto using lift_unit.
 Qed.

 (* We can replace the equality of the two list by the permutation *)
 Lemma equiv_random : forall (Q:mem_rel) E1 E2 t (x1 x2:Var.var t) (d1 d2:E.support t),
  equiv (eq_support d1 d2 /-\ forall_random Q x1 x2 d1)
  E1 [x1 <$- d1] E2 [x2 <$- d2] Q.
 Proof.
  unfold equiv; intros.
  exists (fun m1 m2 => Mlet (sum_support (T.default k t) (E.eval_support d1 m1))
   (fun v => Munit (m1{!x1<--v!}, m2{!x2<--v!}))).
  intros; destruct H as (H1, H2).
  repeat rewrite deno_random; constructor; intros.
  repeat rewrite Mlet_simpl.
  apply mu_stable_eq; simpl; apply ford_eq_intro; intro; trivial.
  repeat rewrite Mlet_simpl.
  rewrite H1; apply mu_stable_eq; simpl; apply ford_eq_intro; intro; trivial.
  apply range_Mlet with (fun v => In v (E.eval_support d1 m1)).
  unfold range; intros; simpl.
  assert (forall n, (n <= (length (E.eval_support d1 m1)))%nat ->
   0 ==
   comp Uplus 0
   (fun n : nat =>
    [1/]1+pred (length (E.eval_support d1 m1)) *
    f (nth n (E.eval_support d1 m1) (T.default k t))) n); auto with arith.
  induction n; simpl; intros; trivial.
  rewrite <- H.
  repeat Usimpl; apply IHn; auto with arith.
  apply nth_In; auto with arith.
  intros; unfold range; simpl; intros.
  apply H0; red; simpl; auto.
 Qed.

 Lemma equiv_random_permut : forall (Q:mem_rel) E1 E2 t (x1 x2:Var.var t)
  (f:forall k, Mem.t k -> Mem.t k -> T.interp k t -> T.interp k t) (d1 d2:E.support t),
  equiv ((permut_support f d1 d2) /-\
   (fun k m1 m2 =>
    forall v, In v (E.eval_support d2 m2) ->
     Q k (m1{!x1 <-- f k m1 m2 v!}) (m2{!x2 <-- v!})))
  E1 [x1 <$- d1] E2 [x2<$-d2] Q.
 Proof.
  unfold equiv; intros.
  exists (fun m1 m2 =>
   Mlet (([[ [x2 <$- d2] ]]) E2 m2)
   (fun m =>
    Munit (m1{! x1 <-- f k m1 m2 (m x2) !}, m))); intros.
  destruct H; constructor; intros.
  rewrite Mlet_simpl, deno_random_elim, deno_random_elim.
  change  (fun x0 : T.interp k t =>
   mu
   (Munit
    (m1 {!x1 <-- f k m1 m2 ((m2 {!x2 <-- x0!}) x2)!}, m2 {!x2 <-- x0!}))
   (fun x : Mem.t k * Mem.t k => f0 (fst x))) with
  (fun x0 : T.interp k t =>f0 (m1 {!x1 <-- f k m1 m2 ((m2 {!x2 <-- x0!}) x2)!})).
  symmetry.
  refine (@sum_dom_permut_eq
    (T.interp k t) (T.interp k t)
    (T.default k t) (T.default k t)
    (E.eval_support d1 m1) (E.eval_support d2 m2)
    (fun x0 : T.interp k t => f0 (m1 {!x1 <-- x0!}))
    (fun x0 : T.interp k t =>
    f0 (m1 {!x1 <-- f k m1 m2 ((m2 {!x2 <-- x0!}) x2)!})) _ ).
  red in H.
  generalize (E.eval_support d1 m1) (E.eval_support d2 m2) H; clear H H0.
  induction 1; constructor; subst; trivial.
  rewrite Mem.get_upd_same; trivial.
  rewrite Mlet_simpl, deno_random_elim, deno_random_elim; trivial.
  rewrite deno_random.
  unfold range; intros.
  repeat rewrite Mlet_simpl.
  change (0 == sum_dom (T.default k t) (E.eval_support d2 m2)
   (fun x : T.interp k t => f0 (m1 {!x1 <-- f k m1 m2 (m2 {!x2 <-- x!} x2)!}, m2 {!x2 <-- x!}))).
  rewrite sum_dom_finite.
  generalize (E.eval_support d2 m2) ([1/]1+pred (length (E.eval_support d2 m2))) H0.
  induction l; simpl; intros; trivial.
  rewrite <- IHl; auto.
  rewrite <- H1; auto.
  red; simpl.
  rewrite Mem.get_upd_same; auto.
 Qed.

 Lemma equiv_union_Modify_pre : forall X1 X2 (P Q Q':mem_rel)
  (P1 P2:forall k, Mem.t k -> Prop) E1 c1 E2 c2,
  (forall k m1 m2, P k m1 m2 -> P1 k m1 /\ P2 k m2) ->
  (forall k m1 m2 m1' m2',
   P k m1 m2 -> Q k m1' m2' ->
   Q' k (m1{!X1 <<- m1'!}) (m2{!X2 <<- m2'!})) ->
  Modify_pre P1 E1 X1 c1 ->
  Modify_pre P2 E2 X2 c2 ->
  equiv P E1 c1 E2 c2 Q ->
  equiv P E1 c1 E2 c2 Q'.
 Proof.
  unfold equiv; intros.
  destruct (H3 k) as (d, Hd).
  exists (fun m1 m2 =>
   Mlet (d m1 m2) (fun p => Munit (m1{!X1<<-fst p!}, m2{!X2<<-snd p!}))).
  intros m1 m2 HP; constructor; simpl; intros.
  rewrite ((Hd _ _ HP).(l_fst) (fun x => f (m1 {!X1 <<- x!}))).
  symmetry; eapply Modify_pre_deno_elim with (k:=k); eauto.
  destruct (H _ _ _ HP); trivial.
  rewrite ((Hd _ _ HP).(l_snd) (fun x => f (m2 {!X2 <<- x!}))).
  symmetry; eapply Modify_pre_deno_elim with (k:= k); eauto.
  destruct (H _ _ _ HP); trivial.
  unfold range; intros; simpl.
  apply (Hd _ _ HP).(l_range); intros; apply H4.
  red; simpl; apply H0; auto.
 Qed.

 Lemma equiv_union_Modify_pre2 : forall X1 X2 (P Q Q':mem_rel)
  (P1 P2:forall k, Mem.t k -> Prop) E1 c1 E2 c2,
  decMR P ->
  (forall k m1 m2, P k m1 m2 -> P1 k m1 /\ P2 k m2) ->
  (forall k m1 m2 m1' m2',
   P k m1 m2 -> Q k m1' m2' -> eeq_mem X1 m1 m1' -> eeq_mem X2 m2 m2' ->
   Q' k m1' m2') ->
  Modify_pre P1 E1 X1 c1 ->
  Modify_pre P2 E2 X2 c2 ->
  equiv P E1 c1 E2 c2 Q ->
  equiv P E1 c1 E2 c2 Q'.
 Proof.
  unfold equiv; intros.
  destruct (H3 k) as (d, Hd).
  assert (forall m1:Mem.t k, P1 k m1 ->
   lift (fun m m'=> m = m' /\ eeq_mem X1 m1 m)
     (Mlet ([[c1]] E1 m1) (fun m => Munit (m, m))) ([[c1]] E1 m1) ([[c1]] E1 m1)).
   constructor; intros.
   rewrite Mlet_simpl; apply (mu_stable_eq ([[c1]] E1 m1)).
   simpl; apply ford_eq_intro; intro; trivial.
   rewrite Mlet_simpl; apply (mu_stable_eq ([[c1]] E1 m1)).
   simpl; apply ford_eq_intro; intro; trivial.
   unfold range; intros; rewrite Mlet_simpl.
   assert (W:= Modify_pre_deno H1 _ H4).
   transitivity (mu (Mlet (([[ c1 ]]) E1 m1) (fun m' : Mem.t k => Munit (m1 {!X1 <<- m'!})))
                   (fun x : Mem.t k => mu (Munit (x, x)) f)).
   rewrite Mlet_simpl.
   rewrite <- (mu_0 (([[ c1 ]]) E1 m1)).
   apply mu_stable_eq; simpl; apply ford_eq_intro; intro; apply H5; split; trivial.
   red; intros; simpl.
   rewrite update_mem_notin; trivial.
   assert (W':= ford_eq_elim (Oeq_sym W)); trivial.
  assert (exists d1,
     forall m1 m2, P k m1 m2 ->
        (lift (fun m1' m2' => Q k m1' m2' /\ eeq_mem X1 m1 m1') (d1 m1 m2)
             (([[ c1 ]]) E1 m1) (([[ c2 ]]) E2 m2))).
   assert (forall (k : nat) (m1 m2 : Mem.t k), P k m1 m2 -> P1 k m1).
    intros k0 m1 m2 HP; destruct (H k0 m1 m2 HP); trivial.
   exists
    (fun  m1 m2 =>
      match X k m1 m2 with
      | left HP =>
        dd' (@mem_eqU k) (H4 m1 (H5 _ _ _ HP)) (Hd _ _ HP)
      | _ => distr0 _
      end).
   intros m1 m3 HP.
   destruct (X k m1 m3); simpl.
   apply lift_trans_discr; auto using mem_eqU_spec, sem_discr.
   intros x y z (W1, W2); subst; tauto.
   elim n; trivial.
  assert (forall m2:Mem.t k, P2 k m2 ->
   lift (fun m m'=> m = m' /\ eeq_mem X2 m2 m')
     (Mlet ([[c2]] E2 m2) (fun m => Munit (m, m))) ([[c2]] E2 m2) ([[c2]] E2 m2)).
   constructor; intros.
   rewrite Mlet_simpl; apply (mu_stable_eq ([[c2]] E2 m2)).
   simpl; apply ford_eq_intro; intro; trivial.
   rewrite Mlet_simpl; apply (mu_stable_eq ([[c2]] E2 m2)).
   simpl; apply ford_eq_intro; intro; trivial.
   unfold range; intros; rewrite Mlet_simpl.
   assert (W:= Modify_pre_deno H2 _ H6).
   transitivity (mu (Mlet (([[ c2 ]]) E2 m2) (fun m' : Mem.t k => Munit (m2 {!X2 <<- m'!})))
                   (fun x : Mem.t k => mu (Munit (x, x)) f)).
   rewrite Mlet_simpl.
   rewrite <- (mu_0 (([[ c2 ]]) E2 m2)).
   apply mu_stable_eq; simpl; apply ford_eq_intro; intro; apply H7; split; trivial.
   red; intros; simpl.
   rewrite update_mem_notin; trivial.
   assert (W':= ford_eq_elim (Oeq_sym W)); trivial.
  destruct H5 as (d1, Hd1).
  assert (forall (k : nat) (m1 m2 : Mem.t k), P k m1 m2 -> P2 k m2).
    intros k0 m1 m2 HP; destruct (H k0 m1 m2 HP); trivial.
  exists
   (fun  m1 m2 =>
      match X k m1 m2 with
      | left HP =>
        dd' (@mem_eqU k) (Hd1 _ _ HP) (H6 m2 (H5 _ _ _ HP))
      | _ => distr0 _
    end).
   intros m1 m3 HP.
   destruct (X k m1 m3); simpl.
   apply lift_trans_discr; auto using mem_eqU_spec, sem_discr.
   intros x y z (W1, W2) (W3, W4); subst; eauto.
   elim n; trivial.
 Qed.

 Lemma equiv_lossless_Modify : forall P X1 X2 M1 M2 E1 c1 E2 c2,
  depend_only_rel P X1 X2 ->
  lossless E1 c1 ->
  lossless E2 c2 ->
  Modify E1 M1 c1 ->
  Modify E2 M2 c2 ->
  Vset.disjoint X1 M1 ->
  Vset.disjoint X2 M2 ->
  equiv P E1 c1 E2 c2 P.
 Proof.
  intros; intro k.
  exists (fun m1 m2 => prod_distr ([[c1]] E1 m1) ([[c2]] E2 m2)); intros.
  constructor; intros.
  rewrite prod_distr_fst.
  unfold lossless in H1; unfold fone; rewrite H1; auto.
  rewrite prod_distr_snd.
  unfold lossless in H0; unfold fone; rewrite H0; auto.
  unfold range, prod_distr; simpl; intros.
  rewrite (Modify_deno_elim H2 (k:=k)).
  transitivity (mu (([[c1]]) E1 m1) (fun _ => 0)).
  symmetry; apply mu_0.
  apply mu_stable_eq; simpl; apply ford_eq_intro; intros m'.
  rewrite (Modify_deno_elim H3 (k:=k)).
  transitivity (mu (([[c2]]) E2 m2) (fun _ => 0)).
  symmetry; apply mu_0.
  apply mu_stable_eq; simpl; apply ford_eq_intro; intros m''.
  apply H7; red; simpl.
  apply H with (3:= H6);
  apply req_mem_sym; apply req_mem_update_disjoint; trivial.
 Qed.

 Lemma equiv_inv_Modify : forall (inv:mem_rel) (X1 X2 M1 M2:Vset.t)
  (P:mem_rel) (E1:env) (c1:cmd) (E2:env) (c2:cmd) (O:Vset.t),
  depend_only_rel inv X1 X2 ->
  Modify E1 M1 c1 ->
  Modify E2 M2 c2 ->
  O [<=] Vset.inter M1 M2 ->
  Vset.disjoint X1 M1 ->
  Vset.disjoint X2 M2 ->
  equiv P E1 c1 E2 c2 (req_mem_rel O trueR) ->
  equiv (P /-\ inv) E1 c1 E2 c2 (req_mem_rel O inv).
 Proof.
  intros; intros k.
  destruct (H5 k) as [d Hd].
  exists (fun m1 m2 =>
   Mlet (d m1 m2) (fun mm => Munit (m1{! M1 <<- fst mm !}, m2{! M2 <<- snd mm!}))).
  intros.
  destruct H6 as [Hreq Hinv].
  destruct (Hd m1 m2 Hreq); clear Hd.
  constructor; intros.

  rewrite (Modify_deno_elim H0).
  apply (l_fst (fun m' => f (m1 {!M1 <<- m'!}))).

  rewrite (Modify_deno_elim H1).
  apply (l_snd (fun m' => f (m2 {!M2 <<- m'!}))).

  apply (range_Mlet _ l_range).
  unfold prodP, req_mem_rel, andR; intros (m1',m2') H6 f Hf; simpl.
  apply Hf; simpl; split.

  intros ? ? ?.
  rewrite update_mem_in, update_mem_in.
  destruct H6; auto.
  eapply Vset.inter_correct_r; apply Vset.subset_correct with (1:=H2); trivial.
  eapply Vset.inter_correct_l; apply Vset.subset_correct with (1:=H2); trivial.

  apply H with (3:=Hinv).
  apply req_mem_sym; apply req_mem_update_disjoint; trivial.
  apply req_mem_sym; apply req_mem_update_disjoint; trivial.
 Qed.

 Definition injR1 (P : forall k, Mem.t k -> Prop) : mem_rel :=
   fun k m1 m2 => P k m1.

 Definition injR2 (P : forall k, Mem.t k -> Prop) : mem_rel :=
   fun k m1 m2 => P k m2.

Lemma lift_trans_l A P (HP : forall (x : A), sumbool (P x) (~P x)) :
  forall B (R : A -> B -> Prop) d d1 d1' d' d2,
 lift (fun (a1 a2: A) => a1 = a2 /\ P a1) d d1 d1' ->
 lift R d' d1' d2 ->
 lift (fun (a : A) (b : B) => R a b /\ P a) d' d1 d2.
Proof.
 intros; constructor.
 intros.

 rewrite H0.(l_fst).
 rewrite <- H.(l_snd).
 rewrite <- H.(l_fst).
 destruct H.
 apply range_eq with (1:= l_range).
 intros (a1,a2) (H1,H2); simpl.
 simpl in *; subst; trivial.

 apply H0.(l_snd).

 assert (range (fun p => P (fst p)) d').
  unfold range.
  intros.
  split.
  auto.
  pose (F := fun a => if HP a then 0 else 1).
  transitivity (mu d' (fun p => F (fst p))).
  apply mu_le_compat; trivial.
  intros p.
  unfold F.
  destruct (HP (fst p)).
  rewrite H1; trivial.
  auto.
  rewrite H0.(l_fst).
  rewrite <- H.(l_snd).
  destruct H.
  unfold range in l_range.
  rewrite <- l_range.
  auto.
  intros (a1,a2) (H2,H3); subst.
  unfold F; simpl in *; subst.
  destruct (HP a2); trivial.
  elim n; trivial.

 unfold range; intros.
 transitivity ((mu d') (fun p => if HP (fst p) then f p else 0)).
 destruct H0.
 unfold range in l_range.
 apply l_range.
 intros.
 destruct (HP (fst x)).
 apply H2.
 split; trivial.
 trivial.

 apply range_eq with (1 := H1).
 intros.
 destruct (HP (fst a)); trivial.
 elim n; trivial.
Qed.

 Lemma equiv_trans_injR1 : forall P1 P Q Q1 E1 c1 E2 c2 (* E1' c1' *),
   (forall k (x : Mem.t k), sumbool (Q1 k x) (~ Q1 k x)) ->
  equiv (Meq /-\ injR1 P1) E1 c1 E1 c1 (Meq /-\ injR1 Q1) ->
  equiv P E1 c1 E2 c2 Q ->
  equiv (P /-\ injR1 P1) E1 c1 E2 c2 (Q /-\ injR1 Q1).
Proof.
  intros; intro k.
  destruct (H k) as (d, Hd); destruct (H0 k) as (d',Hd').
  exists d'; intros m1 m2 (W0, W1).
  unfold andR, injR1.
  eapply lift_trans_l.
  trivial.
  apply lift_weaken with ((Meq /-\ injR1 Q1) k).
  intros m1' m2' (W2, W3); auto.
  apply Hd.
  unfold injR1 in W1.
  split; auto.
  auto.
Qed.

 Lemma equiv_modify : forall (P Q : mem_rel) (E1 E2 : env) (c1 c2 : cmd)
   (t : T.type) (x : Var.var t) (c : forall k, T.interp k t) X,
   ~Vset.mem x X ->
   Modify E1 X c1 ->
   equiv P E1 c1 E2 c2 Q ->
   equiv (P /-\ fun k m1 m2 => E.eval_expr x m1 = c k)
   E1 c1 E2 c2
   (Q /-\ fun k m1 m2 => E.eval_expr x m1 = c k).
 Proof.
  intros.
  apply equiv_trans_injR1.
  intros.
  generalize (T.i_eqb_spec k t (E.eval_expr x x0) (c k)).
  destruct (T.i_eqb k t (E.eval_expr x x0) (c k)); auto.
  intro; exists (fun m1 m2 => Mlet ([[c1]] E1 m1) (fun m' => Munit (m', m'))).
  intros m1 m2 (W0, W1); constructor; intros.
  rewrite Mlet_simpl.
  apply mu_stable_eq.
  refine (ford_eq_intro _); intros; trivial.
  rewrite Mlet_simpl.
  rewrite W0.
  apply mu_stable_eq.
  refine (ford_eq_intro _); intros; trivial.
  rewrite (@Modify_deno E1 X c1 H0), Mcomp.
  apply range_Mlet with (fun _ => True).
  apply range_True.
  unfold range; intros; simpl.
  apply H3.
  split; trivial; simpl.
  unfold injR1 in *.
  rewrite <- W1.
  apply update_mem_notin; trivial.
  trivial.
Qed.

 Lemma equiv_call : forall (P Pf Qf Q:mem_rel) t E1 (x1:Var.var t) f1 a1 E2 (x2:Var.var t) f2 a2,
  (forall k m1 m2, P k m1 m2 ->
   Pf k (init_mem E1 f1 a1 m1) (init_mem E2 f2 a2 m2)) ->
  (forall k m1 m1' m2 m2', P k m1 m2 -> Qf k m1' m2' ->
   Q k (return_mem E1 x1 f1 m1 m1') (return_mem E2 x2 f2 m2 m2')) ->
  equiv Pf E1 (proc_body E1 f1) E2 (proc_body E2 f2) Qf ->
  equiv P E1 [x1 <c- f1 with a1] E2 [x2 <c- f2 with a2] Q.
 Proof.
  unfold equiv; intros.
  destruct (H1 k) as (d, Hd).
  exists (fun m1 m2 =>
   Mlet (d (init_mem E1 f1 a1 m1) (init_mem E2 f2 a2 m2))
   (fun p => Munit (return_mem E1 x1 f1 m1 (fst p), return_mem E2 x2 f2 m2 (snd p)))).
  intros; repeat rewrite deno_call.
  apply lift_Mlet with (Qf k); auto.
  intros m1' m2' HQf; apply lift_unit; auto.
 Qed.

 Lemma equiv_deno : forall P E1 c1 E2 c2 Q,
  equiv P E1 c1 E2 c2 Q ->
  forall k (f g:Mem.t k->U), (forall m1 m2, Q k m1 m2 -> f m1 == g m2) ->
   forall m1 m2, P k m1 m2 -> mu ([[c1]] E1 m1) f == mu ([[c2]] E2 m2) g.
 Proof.
  unfold equiv; intros.
  destruct (H k) as (d, Hd).
  rewrite <- (Hd _ _ H1).(l_fst).
  rewrite <- (Hd _ _ H1).(l_snd).
  apply range_eq with (1:= (Hd _ _ H1).(l_range)).
  intros; apply H0; auto.
 Qed.

 Lemma equiv_deno_le : forall P E1 c1 E2 c2 Q,
  equiv P E1 c1 E2 c2 Q ->
  forall k (f g:Mem.t k->U),
  (forall m1 m2, Q k m1 m2 -> f m1 <= g m2) ->
   forall m1 m2, P k m1 m2 -> mu ([[c1]] E1 m1) f <= mu ([[c2]] E2 m2) g.
 Proof.
  unfold equiv; intros.
  destruct (H k) as (d, Hd).
  rewrite <- (Hd _ _ H1).(l_fst).
  rewrite <- (Hd _ _ H1).(l_snd).
  apply range_le with (1:= (Hd _ _ H1).(l_range)).
  intros; apply H0; auto.
 Qed.

 (** ** Observationnal equivalence with pre and post conditions *)

 (* Three variations of equiv *)

 Definition EqObsRel I P E1 c1 E2 c2 O Q :=
  equiv (req_mem_rel I P) E1 c1 E2 c2 (req_mem_rel O Q).

 Definition EqObsInv P I E1 c1 E2 c2 O :=
  equiv (req_mem_rel I P) E1 c1 E2 c2 (req_mem_rel O P).

 Lemma equiv_trueR_EqObs : forall I E1 c1 E2 c2 O,
  equiv (req_mem_rel I trueR) E1 c1 E2 c2 (req_mem_rel O trueR) ->
  EqObs I E1 c1 E2 c2 O.
 Proof.
  unfold EqObs, req_mem_rel; intros I E1 c1 E2 c2 O; simplMR; trivial.
 Qed.

 Lemma EqObs_equiv_trueR : forall I E1 c1 E2 c2 O,
  EqObs I E1 c1 E2 c2 O ->
  equiv (req_mem_rel I trueR) E1 c1 E2 c2 (req_mem_rel O trueR).
 Proof.
  intros; simplMR; trivial.
 Qed.

 Lemma EqObs_sym : forall I E1 c1 E2 c2 O,
  EqObs I E1 c1 E2 c2 O -> EqObs I E2 c2 E1 c1 O.
 Proof.
  unfold EqObs; intros; apply equiv_sym; auto.
 Qed.

 Lemma EqObs_trans :
   forall I E1 c1 E2 c2 E3 c3 O,
   EqObs I E1 c1 E2 c2 O ->
   EqObs I E2 c2 E3 c3 O ->
   EqObs I E1 c1 E3 c3 O.
 Proof.
  unfold EqObs; intros.
  apply equiv_trans_trans with E2 c2; auto.
 Qed.

 Add Morphism EqObs
  with signature Vset.subset ++> (@eq env) ==> (@eq cmd) ==>
   (@eq env) ==> (@eq cmd) ==> Vset.subset --> impl
  as EqObs_imp_Morph.
 Proof.
  unfold EqObs, flip, impl; intros.
  rewrite H0, <- H; trivial.
 Qed.

 Add Morphism EqObs
  with signature Vset.eq ==> (@eq env) ==> (@eq cmd) ==>
   (@eq env) ==> (@eq cmd) ==> Vset.eq ==> iff
  as EqObs_iff_Morph.
 Proof.
  unfold EqObs; intros.
  rewrite <- H, H0; tauto.
 Qed.

 Add Morphism EqObsInv
  with signature iffMR ==> Vset.subset ++> (@eq env) ==> (@eq cmd) ==>
   (@eq env) ==> (@eq cmd) ==> Vset.subset --> impl
  as EqObsInv_imp_Morph.
 Proof.
  unfold EqObsInv, flip, impl; intros.
  rewrite <- H, <- H0, H1; trivial.
 Qed.

 Add Morphism EqObsInv
  with signature iffMR ==> Vset.eq ==> (@eq env) ==> (@eq cmd) ==>
   (@eq env) ==> (@eq cmd) ==> Vset.eq ==> iff
  as EqObsInv_iff_Morph.
 Proof.
  unfold EqObsInv; intros.
  rewrite <- H, <- H0, H1; tauto.
 Qed.

 Add Morphism EqObsRel
  with signature Vset.subset ++> implMR --> (@eq env) ==> (@eq cmd) ==>
   (@eq env) ==> (@eq cmd) ==> Vset.subset --> implMR ++> impl
  as EqObsRel_imp_Morph.
 Proof.
  unfold EqObsRel, flip, impl; intros.
  rewrite <- H, H1, H0, <- H2; trivial.
 Qed.

 Add Morphism EqObsRel
  with signature Vset.eq ==> iffMR ==> (@eq env) ==> (@eq cmd) ==>
   (@eq env) ==> (@eq cmd) ==> Vset.eq ==> iffMR ==> iff
  as EqObsRel_iff_Morph.
 Proof.
  unfold EqObsRel; intros.
  rewrite <- H, H0, H1, <- H2; split; trivial.
 Qed.

 Lemma EqObs_deno : forall I E1 c1 E2 c2 O,
  EqObs I E1 c1 E2 c2 O ->
  forall k (f g:Mem.t k -> U),
   (forall m1 m2, m1 =={O} m2 -> f m1 == g m2) ->
   forall m1 m2,
    m1 =={I} m2 ->
    mu ([[ c1 ]] E1 m1) f == mu ([[ c2 ]] E2 m2) g.
 Proof.
  intros; apply equiv_deno with (kreq_mem I) (kreq_mem O); trivial.
 Qed.

 Lemma EqObs_deno_same :forall I E1 c1 E2 c2 O,
  EqObs I E1 c1 E2 c2 O ->
  forall k (f g:Mem.t k -> U),
   (forall m1 m2, m1 =={O} m2 -> f m1 == g m2) ->
   forall m, mu ([[ c1 ]] E1 m) f == mu ([[ c2 ]] E2 m) g.
 Proof.
  intros; apply EqObs_deno with I O; trivial.
 Qed.

 Lemma EqObs_assign : forall E1 E2 t (v:Var.var t) (e:E.expr t),
  EqObs (fv_expr e) E1 [v <- e] E2 [v <- e] (Vset.singleton v).
 Proof.
  unfold EqObs; intros; eapply equiv_strengthen; [ | apply equiv_assign].
  unfold kreq_mem; intros; red; red; intros.
  apply Vset.singleton_complete in H0.
  inversion H0; simpl; repeat rewrite Mem.get_upd_same.
  apply EqObs_e_fv_expr; trivial.
 Qed.

 Lemma EqObs_random : forall E1 E2 t (v:Var.var t) (d:E.support t),
  EqObs (fv_distr d) E1 [v <$- d] E2 [v <$- d] (Vset.singleton v).
 Proof.
  unfold EqObs; intros; eapply equiv_strengthen; [ | apply equiv_random].
  unfold kreq_mem; intros; red; intros; split.
  unfold eq_support; apply EqObs_d_fv_expr; trivial.
  red; red; intros.
  apply Vset.singleton_complete in H1.
  inversion H1; simpl; repeat rewrite Mem.get_upd_same; trivial.
 Qed.

 (** ** Procedure info used for equivalence *)

 Record dproc_eq_refl_info : Type :=
  {
   dpi_mod : Vset.t;      (* modified globals variables *)
   dpi_input : Vset.t;    (* global variables *)
   dpi_params : Vset.t;   (* local variables  *)
   dpi_output : Vset.t;   (* global variables *)
   dpi_lossless : bool
  }.

 Record sproc_eq_refl_info (E:env) (t:T.type) (f:Proc.proc t) (data:dproc_eq_refl_info) : Prop :=
  {
   slossless_spec : data.(dpi_lossless) -> lossless E (proc_body E f);
   sinput_global : forall x, Vset.mem x data.(dpi_input) -> Var.is_global x;
   sparams_subset : data.(dpi_params) [<=] Vset_of_var_decl (proc_params E f);
   soutput_global : forall x, Vset.mem x data.(dpi_output) -> Var.is_global x;
   smod_global : forall x, Vset.mem x data.(dpi_mod) -> Var.is_global x;
   smod_spec : exists L,
    (forall x, Vset.mem x L -> Var.is_local x) /\
    Modify E (Vset.union L data.(dpi_mod)) (proc_body E f);
   soutput_subset : data.(dpi_output) [<=] data.(dpi_mod);
    spi_spec :
    exists ls,
     (forall x, Vset.mem x ls -> Var.is_local x) /\
     EqObs (Vset.union data.(dpi_input) data.(dpi_params))
     E (proc_body E f) E (proc_body E f) (Vset.union ls data.(dpi_output)) /\
     EqObs_e (Vset.union (Vset.union ls data.(dpi_output))
      (Vset.diff data.(dpi_input) data.(dpi_mod)))
     (proc_res E f) (proc_res E f)
  }.

 Record proc_eq_refl_info (E:env) (t:T.type) (f:Proc.proc t) : Type :=
  {
   dpi : dproc_eq_refl_info;
   spi : sproc_eq_refl_info E f dpi
  }.

 Definition pi_mod E t f (pi:@proc_eq_refl_info E t f) :=
  pi.(dpi).(dpi_mod).

 Definition pi_input E t f (pi:@proc_eq_refl_info E t f) :=
  pi.(dpi).(dpi_input).

 Definition pi_params E t f (pi:@proc_eq_refl_info E t f) :=
  pi.(dpi).(dpi_params).

 Definition pi_output E t f (pi:@proc_eq_refl_info E t f) :=
  pi.(dpi).(dpi_output).

 Definition pi_lossless E t f (pi:@proc_eq_refl_info E t f) :=
  pi.(dpi).(dpi_lossless).

 Definition pi_lossless_spec E t f (pi:@proc_eq_refl_info E t f) :
  (pi_lossless pi) -> lossless E (proc_body E f) :=
  pi.(spi).(slossless_spec).

 Definition input_global E t f (pi:@proc_eq_refl_info E t f) :
  forall x, Vset.mem x (pi_input pi) -> Var.is_global x :=
   pi.(spi).(sinput_global).

 Definition params_subset E t f (pi:@proc_eq_refl_info E t f) :
  (pi_params pi) [<=] Vset_of_var_decl (proc_params E f):=
  pi.(spi).(sparams_subset).

 Definition output_global E t f (pi:@proc_eq_refl_info E t f) :
  forall x, Vset.mem x (pi_output pi) -> Var.is_global x :=
   pi.(spi).(soutput_global).

 Definition mod_global E t f (pi:@proc_eq_refl_info E t f) :
  forall x, Vset.mem x (pi_mod pi) -> Var.is_global x :=
   pi.(spi).(smod_global).

 Definition mod_spec E t f (pi:@proc_eq_refl_info E t f) :
  exists L,
   (forall x, Vset.mem x L -> Var.is_local x) /\
   Modify E (Vset.union L (pi_mod pi)) (proc_body E f) :=
   pi.(spi).(smod_spec).

 Definition output_subset E t f (pi:@proc_eq_refl_info E t f) :
  (pi_output pi) [<=] (pi_mod pi):=
  pi.(spi).(soutput_subset).

 Definition pi_spec E t f (pi:@proc_eq_refl_info E t f) :
  exists ls,
   (forall x, Vset.mem x ls -> Var.is_local x) /\
   EqObs (Vset.union (pi_input pi) (pi_params pi))
   E (proc_body E f) E (proc_body E f) (Vset.union ls (pi_output pi)) /\
   EqObs_e (Vset.union (Vset.union ls (pi_output pi))
    (Vset.diff (pi_input pi) (pi_mod pi)))
   (proc_res E f) (proc_res E f) :=
   pi.(spi).(spi_spec).

 Lemma pi_spec_call_1 : forall E t (f:Proc.proc t) (pi:proc_eq_refl_info E f),
  forall (d1 d2:Var.var t) args1 args2 I,
   EqObs_args (proc_params E f) args1 (proc_params E f) args2 (pi_params pi) I ->
   pi_input pi [<=] I ->
   equiv (kreq_mem I) E [d1 <c- f with args1] E [d2 <c- f with args2]
   (fun k m1 m2 =>
    m1 =={Vset.remove d1
     (Vset.remove d2 (Vset.union (pi_output pi) (Vset.diff I (pi_mod pi))))} m2 /\
    E.eval_expr d1 m1 = E.eval_expr d2 m2).
 Proof.
  intros.
  apply equiv_call with
   (Pf:= kreq_mem
    (Vset.union (Vset.union (pi_input pi) (pi_params pi))
     (Vset.diff (get_globals I) (pi_mod pi))))
   (Qf := fun k m1 m2 =>
    m1 =={Vset.union (pi_output pi) (Vset.diff (get_globals I) (pi_mod pi))} m2 /\
    E.eval_expr (proc_res E f) m1 = E.eval_expr (proc_res E f) m2).
  (* init *)
  unfold kreq_mem; intros.
  eapply req_mem_weaken;[ | apply EqObs_args_correct with (1:= H)]; trivial.
  rewrite (VsetP.union_sym (pi_input pi)).
  rewrite VsetP.union_assoc; apply VsetP.subset_union_ctxt; auto with set.
  apply VsetP.subset_trans with (Vset.union (get_globals I) (get_globals I)).
  apply VsetP.subset_union_ctxt; auto with set.
  apply Vset.subset_complete; intros.
  apply get_globals_complete.
  apply Vset.subset_correct with (1:= H0); trivial.
  apply (input_global pi); trivial.
  rewrite VsetP.union_idem; auto with set.
  (* post *)
  intros k m1 m1' m2 m2' H1 (H2,H3); split.
  red; intros.
  repeat rewrite VsetP.remove_spec in H4; destruct H4 as ((H4,H5),H6).
  rewrite VsetP.union_spec, VsetP.diff_spec in H4.
  case_eq (Var.is_global x); intros.
  repeat rewrite return_mem_global; trivial.
  apply H2; rewrite VsetP.union_spec, VsetP.diff_spec; intuition.
  right; split; trivial.
  apply get_globals_complete; trivial.
  assert (Var.is_local x) by (unfold Var.is_local; rewrite H7; trivial).
  repeat rewrite return_mem_local; trivial.
  apply H1; intuition.
  apply output_global in H9; rewrite H7 in H9; trivialb.
  simpl. repeat rewrite return_mem_dest; trivial.
  (* body *)
  destruct (mod_spec pi) as (L, (H1,H2)).
  destruct (pi_spec pi) as (ls, (H3,(H4,H5))).
  assert (Modify_pre (fun _ _ => True) E
   (Vset.union (Vset.union L (pi_mod pi)) ls) (proc_body E f)).
  apply Modify_Modify_pre.
  apply Modify_weaken with (1:=H2); auto with set.
  apply equiv_union_Modify_pre with (3:= H6) (4:=H6)
   (Q:= kreq_mem (Vset.union ls (pi_output pi))); auto.
  unfold kreq_mem; intros; split.
  red; intros t0 x H9; rewrite VsetP.union_spec, VsetP.diff_spec in H9; destruct H9.
  assert (Vset.mem x (Vset.union (Vset.union L (pi_mod pi)) ls)).
  repeat rewrite VsetP.union_spec; left; right.
  apply Vset.subset_correct with (1:= output_subset pi); trivial.
  repeat rewrite update_mem_in; trivial.
  apply H8; rewrite VsetP.union_spec; auto.
  assert (~Vset.mem x (Vset.union (Vset.union L (pi_mod pi)) ls)).
  destruct H9; repeat rewrite (VsetP.union_spec).
  apply get_globals_spec in H9.
  intros [ [W|W] | W]; auto.
  apply H1 in W; unfold Var.is_local in W; rewrite H9 in W; discriminate.
  apply H3 in W; unfold Var.is_local in W; rewrite H9 in W; discriminate.
  repeat rewrite update_mem_notin; trivial.
  apply H7; rewrite VsetP.union_spec,VsetP.diff_spec; auto.
  apply H5.
  repeat apply req_mem_union; red; intros.
  repeat rewrite update_mem_in; auto with set.
  assert (W:= Vset.subset_correct (output_subset pi) _ H9).
  repeat rewrite update_mem_in; auto with set.
  rewrite VsetP.diff_spec in H9; destruct H9.
  assert (W1:= input_global pi _ H9).
  assert (~Vset.mem x (Vset.union (Vset.union L (pi_mod pi)) ls)).
  repeat rewrite (VsetP.union_spec); intros [ [W|W] | W]; auto.
  apply H1 in W; unfold Var.is_local in W; rewrite W1 in W; discriminate.
  apply H3 in W; unfold Var.is_local in W; rewrite W1 in W; discriminate.
  repeat rewrite update_mem_notin; trivial; auto with set.
  apply equiv_strengthen with (2:=H4); unfold kreq_mem; intros.
  apply req_mem_weaken with (2:=H7); auto with set.
 Qed.

 Lemma pi_spec_call : forall E t (f:Proc.proc t) (pi:proc_eq_refl_info E f),
  forall (d:Var.var t) args I,
   EqObs_args (proc_params E f) args (proc_params E f) args (pi_params pi) I ->
   pi_input pi [<=] I ->
   EqObs I E [d <c- f with args] E [d<c- f with args]
   (Vset.union (Vset.add d (pi_output pi)) (Vset.diff I (pi_mod pi))).
 Proof.
  intros; unfold EqObs.
  eapply equiv_weaken;[ | apply (pi_spec_call_1 pi)]; auto.
  intros k m1 m2 (H1,H2) tx x Hin.
  destruct (VarP.eq_dec d x); subst.
  inversion e; simpl; trivial.
  apply H1.
  repeat (rewrite VsetP.remove_spec; split; trivial).
  rewrite <- VsetP.add_union_comm,VsetP.add_spec in Hin; destruct Hin; trivial.
  elim (n H3).
 Qed.

 Lemma mod_spec_call : forall E t (f:Proc.proc t)
  (pif: proc_eq_refl_info E f) (d:Var.var t) args,
  Modify E (Vset.add d (pi_mod pif)) [d <c- f with args].
 Proof.
  intros; destruct (mod_spec pif) as (L,(H,H0)).
  eapply Modify_weaken;[ apply Modify_call with (1:=H0) | ].
  apply VsetP.subset_add_ctxt.
  apply Vset.subset_complete; intros.
  assert (W:=get_globals_spec _ _ H1).
  assert (Vset.mem x (Vset.union L (pi_mod pif))).
  apply Vset.subset_correct with
   (1:= get_globals_subset(Vset.union L (pi_mod pif))); trivial.
  rewrite VsetP.union_spec in H2; destruct H2; trivial.
  apply H in H2; unfold Var.is_local in H2; rewrite W in H2; discriminate.
 Qed.

 Lemma Vset_of_var_decl_ind : forall (P:forall t, Var.var t -> Prop) lt
  (lv:var_decl lt),
  (forall t (x:Var.var t), DIn t x lv -> P t x) ->
  forall t (x:Var.var t), Vset.mem x (Vset_of_var_decl lv) -> P t x.
 Proof.
  unfold Vset_of_var_decl; induction lv; simpl; intros; trivialb.
  rewrite VsetP.add_spec in H0; destruct H0; auto.
  apply H; left; inversion H0; constructor.
 Qed.

 Lemma params_local : forall E t (f:Proc.proc t) (pif:proc_eq_refl_info E f),
  forall x, Vset.mem x (pi_params pif) -> Var.is_local x.
 Proof.
  intros; destruct x as (tx, x).
  refine (@Vset_of_var_decl_ind
   (fun t x => is_true (Var.is_local x)) _ (proc_params E f) _ tx x _).
  intros; rewrite <- Var.vis_local_local.
  unfold proc_params in H0.
  apply proc_params_local with (p:=f) (1:= H0).
  apply (Vset.subset_correct (params_subset pif)); trivial.
 Qed.

 Definition eq_refl_info E :=
  forall t (f:Proc.proc t), option (proc_eq_refl_info E f).

 (** Probability *)

 Lemma EqObs_Pr2 : forall I E1 c1 E2 c2 O,
  EqObs I E1 c1 E2 c2 O ->
  forall e, fv_expr e [<=] O ->
   forall k (m1 m2:Mem.t k), m1 =={I} m2 -> Pr E1 c1 m1 (EP k e) == Pr E2 c2 m2 (EP k e).
 Proof.
  unfold Pr; intros.
  apply EqObs_deno with I O; trivial.
  unfold charfun,restr, EP; intros.
  assert (W := req_mem_weaken H0 H2).
  rewrite (EqObs_e_fv_expr e W); trivial.
 Qed.

 Lemma EqObs_Pr : forall I E1 c1 E2 c2 e,
  EqObs I E1 c1 E2 c2 (fv_expr e) ->
  forall k m, Pr E1 c1 m (EP k e) == Pr E2 c2 m (EP k e).
 Proof.
  intros; eapply EqObs_Pr2; eauto with set.
 Qed.

End Make.

author: EasyCrypt

repo: certicrypt

save_path: github-repos/coq/EasyCrypt-certicrypt


text:
(** * Prop: Propositions and Evidence *)

Require Export Logic.
Check orb.
Check plus_swap.
(* ####################################################### *)
(** * Inductively Defined Propositions *)

(** In chapter [Basics] we defined a _function_ [evenb] that tests a
    number for evenness, yielding [true] if so.  We can use this
    function to define the _proposition_ that some number [n] is
    even: *)

Definition even (n:nat) : Prop :=
  evenb n = true.

Eval compute in even 3.

(** That is, we can define "[n] is even" to mean "the function [evenb]
    returns [true] when applied to [n]."

    Note that here we have given a name
    to a proposition using a [Definition], just as we have
    given names to expressions of other sorts. This isn't a fundamentally
    new kind of proposition;  it is still just an equality. *)

(** Another alternative is to define the concept of evenness
    directly.  Instead of going via the [evenb] function ("a number is
    even if a certain computation yields [true]"), we can say what the
    concept of evenness means by giving two different ways of
    presenting _evidence_ that a number is even. *)

Inductive ev : nat -> Prop :=
  | ev_0 : ev O
  | ev_SS : forall n:nat, ev n -> ev (S (S n)).
Eval compute in ev 1.

(** The first line declares that [ev] is a proposition -- or,
    more formally, a family of propositions "indexed by" natural
    numbers.  (That is, for each number [n], the claim that "[n] is
    even" is a proposition.)  Such a family of propositions is
    often called a _property_ of numbers.

    The last two lines declare the two ways to give evidence that a
    number [m] is even.  First, [0] is even, and [ev_0] is evidence
    for this.  Second, if [m = S (S n)] for some [n] and we can give
    evidence [e] that [n] is even, then [m] is also even, and [ev_SS n
    e] is the evidence.
*)

(** **** Exercise: 1 star (double_even)  *)

Theorem double_even : forall n,
  ev (double n).
Proof.
  intros n.
  induction n.
  Case "n=0".
  simpl. apply ev_0.
  Case "n=S n".
  simpl. apply ev_SS.
  apply IHn.
Qed.
(** [] *)

(* ##################################################### *)

(** For [ev], we had already defined [even] as a function (returning a
   boolean), and then defined an inductive relation that agreed with
   it. However, we don't necessarily need to think about propositions
   first as boolean functions, we can start off with the inductive
   definition.
*)

(** As another example of an inductively defined proposition, let's
    define a simple property of natural numbers -- we'll call it
    "[beautiful]." *)

(** Informally, a number is [beautiful] if it is [0], [3], [5], or the
    sum of two [beautiful] numbers.

    More pedantically, we can define [beautiful] numbers by giving four
    rules:

       - Rule [b_0]: The number [0] is [beautiful].
       - Rule [b_3]: The number [3] is [beautiful].
       - Rule [b_5]: The number [5] is [beautiful].
       - Rule [b_sum]: If [n] and [m] are both [beautiful], then so is
         their sum. *)

(** We will see many definitions like this one during the rest
    of the course, and for purposes of informal discussions, it is
    helpful to have a lightweight notation that makes them easy to
    read and write.  _Inference rules_ are one such notation: *)
(**
                              -----------                               (b_0)
                              beautiful 0

                              ------------                              (b_3)
                              beautiful 3

                              ------------                              (b_5)
                              beautiful 5

                       beautiful n     beautiful m
                       ---------------------------                      (b_sum)
                              beautiful (n+m)
*)

(** *** *)
(** Each of the textual rules above is reformatted here as an
    inference rule; the intended reading is that, if the _premises_
    above the line all hold, then the _conclusion_ below the line
    follows.  For example, the rule [b_sum] says that, if [n] and [m]
    are both [beautiful] numbers, then it follows that [n+m] is
    [beautiful] too.  If a rule has no premises above the line, then
    its conclusion holds unconditionally.

    These rules _define_ the property [beautiful].  That is, if we
    want to convince someone that some particular number is [beautiful],
    our argument must be based on these rules.  For a simple example,
    suppose we claim that the number [5] is [beautiful].  To support
    this claim, we just need to point out that rule [b_5] says so.
    Or, if we want to claim that [8] is [beautiful], we can support our
    claim by first observing that [3] and [5] are both [beautiful] (by
    rules [b_3] and [b_5]) and then pointing out that their sum, [8],
    is therefore [beautiful] by rule [b_sum].  This argument can be
    expressed graphically with the following _proof tree_: *)
(**
         ----------- (b_3)   ----------- (b_5)
         beautiful 3         beautiful 5
         ------------------------------- (b_sum)
                   beautiful 8
*)
(** *** *)
(**
    Of course, there are other ways of using these rules to argue that
    [8] is [beautiful], for instance:
         ----------- (b_5)   ----------- (b_3)
         beautiful 5         beautiful 3
         ------------------------------- (b_sum)
                   beautiful 8
*)

(** **** Exercise: 1 star (varieties_of_beauty)  *)
(** How many different ways are there to show that [8] is [beautiful]? *)

(* FILL IN HERE *)
(** [] *)

(* ####################################################### *)
(** ** Constructing Evidence *)

(** In Coq, we can express the definition of [beautiful] as
    follows: *)

Inductive beautiful : nat -> Prop :=
  b_0   : beautiful 0
| b_3   : beautiful 3
| b_5   : beautiful 5
| b_sum : forall n m, beautiful n -> beautiful m -> beautiful (n+m).

(** *** *)
(**
    The rules introduced this way have the same status as proven
    theorems; that is, they are true axiomatically.
    So we can use Coq's [apply] tactic with the rule names to prove
    that particular numbers are [beautiful].  *)

Theorem three_is_beautiful: beautiful 3.
Proof.
   (* This simply follows from the rule [b_3]. *)
   apply b_3.
Qed.

Theorem eight_is_beautiful: beautiful 8.
Proof.
   (* First we use the rule [b_sum], telling Coq how to
      instantiate [n] and [m]. *)
   apply b_sum with (n:=3) (m:=5).
   (* To solve the subgoals generated by [b_sum], we must provide
      evidence of [beautiful 3] and [beautiful 5]. Fortunately we
      have rules for both. *)
   apply b_3.
   apply b_5.
Qed.

(** *** *)
(** As you would expect, we can also prove theorems that have
hypotheses about [beautiful]. *)

Theorem beautiful_plus_eight: forall n, beautiful n -> beautiful (8+n).
Proof.
  intros n B.
  apply b_sum with (n:=8) (m:=n).
  apply eight_is_beautiful.
  apply B.
Qed.

(** **** Exercise: 2 stars (b_times2)  *)
Theorem b_times2: forall n, beautiful n -> beautiful (2*n).
Proof.
  intros n B.
  simpl.
  apply b_sum with (n:=n) (m:=(n+0)).
  apply B.
  rewrite -> plus_0_r.
  apply B.
Qed.
(** [] *)

(** **** Exercise: 3 stars (b_timesm)  *)
Theorem b_timesm: forall n m, beautiful n -> beautiful (m*n).
Proof.
  intros n m B.
  induction m.
  Case "m=0".
  simpl. apply b_0.
  Case "m=S m".
  simpl.
  apply b_sum with (n:=n) (m:=m*n).
  apply B.
  apply IHm.
Qed.
(** [] *)

(* ####################################################### *)
(** * Using Evidence in Proofs *)
(** ** Induction over Evidence *)

(** Besides _constructing_ evidence that numbers are beautiful, we can
    also _reason about_ such evidence. *)

(** The fact that we introduced [beautiful] with an [Inductive]
    declaration tells Coq not only that the constructors [b_0], [b_3],
    [b_5] and [b_sum] are ways to build evidence, but also that these
    four constructors are the _only_ ways to build evidence that
    numbers are beautiful. *)

(** In other words, if someone gives us evidence [E] for the assertion
    [beautiful n], then we know that [E] must have one of four shapes:

      - [E] is [b_0] (and [n] is [O]),
      - [E] is [b_3] (and [n] is [3]),
      - [E] is [b_5] (and [n] is [5]), or
      - [E] is [b_sum n1 n2 E1 E2] (and [n] is [n1+n2], where [E1] is
        evidence that [n1] is beautiful and [E2] is evidence that [n2]
        is beautiful). *)

(** *** *)
(** This permits us to _analyze_ any hypothesis of the form [beautiful
    n] to see how it was constructed, using the tactics we already
    know.  In particular, we can use the [induction] tactic that we
    have already seen for reasoning about inductively defined _data_
    to reason about inductively defined _evidence_.

    To illustrate this, let's define another property of numbers: *)

Inductive gorgeous : nat -> Prop :=
  g_0 : gorgeous 0
| g_plus3 : forall n, gorgeous n -> gorgeous (3+n)
| g_plus5 : forall n, gorgeous n -> gorgeous (5+n).

(** **** Exercise: 1 star (gorgeous_tree)  *)
(** Write out the definition of [gorgeous] numbers using inference rule
    notation.

(* FILL IN HERE *)
[]
*)
Check g_plus3.

(** **** Exercise: 1 star (gorgeous_plus13)  *)
Theorem gorgeous_plus13: forall n,
  gorgeous n -> gorgeous (13+n).
Proof.
  intros n G.
  apply g_plus5 with (n:=8+n). apply g_plus3 with (n:=5+n).
  apply g_plus5 with (n:=n). apply G.
Qed.
(** [] *)

(** *** *)
(** It seems intuitively obvious that, although [gorgeous] and
    [beautiful] are presented using slightly different rules, they are
    actually the same property in the sense that they are true of the
    same numbers.  Indeed, we can prove this. *)

Theorem gorgeous__beautiful_FAILED : forall n,
  gorgeous n -> beautiful n.
Proof.
   intros. induction n as [| n'].
   Case "n = 0". apply b_0.
   Case "n = S n'". (* We are stuck! *)
Abort.

(** The problem here is that doing induction on [n] doesn't yield a
    useful induction hypothesis. Knowing how the property we are
    interested in behaves on the predecessor of [n] doesn't help us
    prove that it holds for [n]. Instead, we would like to be able to
    have induction hypotheses that mention other numbers, such as [n -
    3] and [n - 5]. This is given precisely by the shape of the
    constructors for [gorgeous]. *)

(** *** *)

(** Let's see what happens if we try to prove this by induction on the evidence [H]
   instead of on [n]. *)

Theorem gorgeous__beautiful : forall n,
  gorgeous n -> beautiful n.
Proof.
   intros n H.
   induction H as [|n'|n'].
   Case "g_0".
       apply b_0.
   Case "g_plus3".
       apply b_sum with (n:=3) (m:=n'). apply b_3.
       apply IHgorgeous.
   Case "g_plus5".
       apply b_sum with (n:=5) (m:=n'). apply b_5. apply IHgorgeous.
Qed.

(* These exercises also require the use of induction on the evidence. *)

(** **** Exercise: 2 stars (gorgeous_sum)  *)
Theorem gorgeous_sum : forall n m,
  gorgeous n -> gorgeous m -> gorgeous (n + m).
Proof.
  intros n m H G.
  induction H as [|b|c].
  Case "g_0".
  simpl. apply G.
  Case "g_plus3".
  apply g_plus3 with (n:=b+m). apply IHgorgeous.
  Case "g_plus5".
  apply g_plus5 with (n:=c+m). apply IHgorgeous.
Qed.
(** [] *)

(** **** Exercise: 3 stars, advanced (beautiful__gorgeous)  *)
Theorem beautiful__gorgeous : forall n, beautiful n -> gorgeous n.
Proof.
  intros n H.
  induction H as [| | |n'].
  Case "b_0".
  apply g_0.
  Case "b_3".
  apply g_plus3 with (n:=0). apply g_0.
  Case "b_5".
  apply g_plus5 with (n:=0). apply g_0.
  Case "b_sum".
  apply gorgeous_sum with (n:=n') (m:=m).
  apply IHbeautiful1. apply IHbeautiful2.
Qed.
(** [] *)

(** **** Exercise: 3 stars, optional (g_times2)  *)
(** Prove the [g_times2] theorem below without using [gorgeous__beautiful].
    You might find the following helper lemma useful. *)

Lemma helper_g_times2 : forall x y z, x + (z + y) = z + x + y.
Proof.
  intros x y z.
  assert (H1: x+(z+y)=x+z+y).
  apply plus_assoc.
  rewrite -> H1.
  assert (H2: x+z=z+x).
  apply plus_comm.
  rewrite -> H2.
  reflexivity.
Qed.

Theorem g_times2: forall n, gorgeous n -> gorgeous (2*n).
Proof.
   intros n H. simpl.
   induction H.
   Case "g_0".
   simpl. apply g_0.
   Case "g_3".
   assert (H1:3+n+0=3+(n+0)).
   symmetry. apply plus_assoc.
   rewrite H1.
   rewrite helper_g_times2 with (x:=3+n) (z:=3) (y:=n+0).
   apply g_plus3 with (n:=3+n+(n+0)).
   apply g_plus3 with (n:=n+(n+0)).
   apply IHgorgeous.
   Case "g_5".
   assert (H2:5+n+0=5+(n+0)).
   symmetry. apply plus_assoc.
   rewrite H2.
   rewrite helper_g_times2 with (x:=5+n) (z:=5) (y:=n+0).
   apply g_plus5 with (n:=5+n+(n+0)).
   apply g_plus5 with (n:=n+(n+0)).
   apply IHgorgeous.
Qed.
(** [] *)

(** Here is a proof that the inductive definition of evenness implies
the computational one. *)

Theorem ev__even : forall n,
  ev n -> even n.
Proof.
  intros n E. induction E as [| n' E'].
  Case "E = ev_0".
    unfold even. reflexivity.
  Case "E = ev_SS n' E'".
    unfold even. simpl.
    unfold even in IHE'. apply IHE'.
Qed.

(** **** Exercise: 1 star (ev__even)  *)
(** Could this proof also be carried out by induction on [n] instead
    of [E]?  If not, why not? *)

(* FILL IN HERE *)
(** [] *)

(** Intuitively, the induction principle [ev n] evidence [ev n] is
    similar to induction on [n], but restricts our attention to only
    those numbers for which evidence [ev n] could be generated. *)

(** **** Exercise: 1 star (l_fails)  *)
(** The following proof attempt will not succeed.
     Theorem l : forall n,
       ev n.
     Proof.
       intros n. induction n.
         Case "O". simpl. apply ev_0.
         Case "S".
           ...
   Intuitively, we expect the proof to fail because not every
   number is even. However, what exactly causes the proof to fail?

(* FILL IN HERE *)
*)
(** [] *)

(** Here's another exercise requiring induction on evidence. *)
(** **** Exercise: 2 stars (ev_sum)  *)

Theorem ev_sum : forall n m,
   ev n -> ev m -> ev (n+m).
Proof.
  intros n m.
  intros H.
  induction H as [| H'].
  Case "H_ev_0".
  intros G.
  simpl. apply G.
  Case "H_ev_SS".
  intros G.
  destruct G as [| G'].
  SCase "G_ev_0".
  simpl. rewrite plus_0_r.
  apply ev_SS. apply H.
  SCase "G_en_SS".
  simpl. apply ev_SS.
  apply IHev. apply ev_SS.
  apply G.
Qed.
(** [] *)

(* ####################################################### *)
(** ** Inversion on Evidence *)

(** Having evidence for a proposition is useful while proving, because we
   can _look_ at that evidence for more information. For example, consider
    proving that, if [n] is even, then [pred (pred n)] is
    too.  In this case, we don't need to do an inductive proof.  Instead
    the [inversion] tactic provides all of the information that we need.

 *)

Theorem ev_minus2: forall n,  ev n -> ev (pred (pred n)).
Proof.
  intros n E.
  inversion E as [| n' E'].
  Case "E = ev_0". simpl. apply ev_0.
  Case "E = ev_SS n' E'". simpl. apply E'.  Qed.

(** **** Exercise: 1 star, optional (ev_minus2_n)  *)
(** What happens if we try to use [destruct] on [n] instead of [inversion] on [E]? *)

(* FILL IN HERE *)
(** [] *)

(** *** *)
(** Here is another example, in which [inversion] helps narrow down to
the relevant cases. *)

Theorem SSev__even : forall n,
  ev (S (S n)) -> ev n.
Proof.
  intros n E.
  inversion E as [| n' E'].
  apply E'. Qed.

(** ** The Inversion Tactic Revisited *)

(** These uses of [inversion] may seem a bit mysterious at first.
    Until now, we've only used [inversion] on equality
    propositions, to utilize injectivity of constructors or to
    discriminate between different constructors.  But we see here
    that [inversion] can also be applied to analyzing evidence
    for inductively defined propositions.

    (You might also expect that [destruct] would be a more suitable
    tactic to use here. Indeed, it is possible to use [destruct], but
    it often throws away useful information, and the [eqn:] qualifier
    doesn't help much in this case.)

    Here's how [inversion] works in general.  Suppose the name
    [I] refers to an assumption [P] in the current context, where
    [P] has been defined by an [Inductive] declaration.  Then,
    for each of the constructors of [P], [inversion I] generates
    a subgoal in which [I] has been replaced by the exact,
    specific conditions under which this constructor could have
    been used to prove [P].  Some of these subgoals will be
    self-contradictory; [inversion] throws these away.  The ones
    that are left represent the cases that must be proved to
    establish the original goal.

    In this particular case, the [inversion] analyzed the construction
    [ev (S (S n))], determined that this could only have been
    constructed using [ev_SS], and generated a new subgoal with the
    arguments of that constructor as new hypotheses.  (It also
    produced an auxiliary equality, which happens to be useless here.)
    We'll begin exploring this more general behavior of inversion in
    what follows. *)

(** **** Exercise: 1 star (inversion_practice)  *)
Theorem SSSSev__even : forall n,
  ev (S (S (S (S n)))) -> ev n.
Proof.
  intros n H.
  inversion H as [| H'].
  inversion H1 as [| H1'].
  apply H3.
Qed.

(** The [inversion] tactic can also be used to derive goals by showing
    the absurdity of a hypothesis. *)

Theorem even5_nonsense :
  ev 5 -> 2 + 2 = 9.
Proof.
  intros.
  inversion H. inversion H1. inversion H3.
Qed.
(** [] *)

(** **** Exercise: 3 stars, advanced (ev_ev__ev)  *)
(** Finding the appropriate thing to do induction on is a
    bit tricky here: *)

Theorem ev_ev__ev : forall n m,
  ev (n+m) -> ev n -> ev m.
Proof.
  intros n m E1 E2.
  generalize dependent E1.
  induction E2.
  simpl. intros E. apply E.
  simpl. intros H.
  apply IHE2. inversion H.
  apply H1.
Qed.
(** [] *)

(** **** Exercise: 3 stars, optional (ev_plus_plus)  *)
(** Here's an exercise that just requires applying existing lemmas.  No
    induction or even case analysis is needed, but some of the rewriting
    may be tedious. *)

Theorem ev_plus_plus : forall n m p,
  ev (n+m) -> ev (n+p) -> ev (m+p).
Proof.
  intros n m p Hm Hp.
  apply ev_sum with (n:=n+m) (m:=n+p) in Hm.
  replace (n+m+(n+p)) with ((n+n)+(m+p)) in Hm.
  apply ev_ev__ev with (n:=n+n) in Hm.
  apply Hm.
  rewrite <- double_plus.
  apply double_even.
  rewrite <- plus_assoc.
  replace (n+(m+p)) with (m+(n+p)).
  rewrite <- plus_assoc.
  reflexivity.
  apply plus_swap.
  apply Hp.
Qed.
(** [] *)

(* ####################################################### *)
(** * Discussion and Variations *)
(** ** Computational vs. Inductive Definitions *)

(** We have seen that the proposition "[n] is even" can be
    phrased in two different ways -- indirectly, via a boolean testing
    function [evenb], or directly, by inductively describing what
    constitutes evidence for evenness.  These two ways of defining
    evenness are about equally easy to state and work with.  Which we
    choose is basically a question of taste.

    However, for many other properties of interest, the direct
    inductive definition is preferable, since writing a testing
    function may be awkward or even impossible.

    One such property is [beautiful].  This is a perfectly sensible
    definition of a set of numbers, but we cannot translate its
    definition directly into a Coq Fixpoint (or into a recursive
    function in any other common programming language).  We might be
    able to find a clever way of testing this property using a
    [Fixpoint] (indeed, it is not too hard to find one in this case),
    but in general this could require arbitrarily deep thinking.  In
    fact, if the property we are interested in is uncomputable, then
    we cannot define it as a [Fixpoint] no matter how hard we try,
    because Coq requires that all [Fixpoint]s correspond to
    terminating computations.

    On the other hand, writing an inductive definition of what it
    means to give evidence for the property [beautiful] is
    straightforward. *)

(* ####################################################### *)
(** ** Parameterized Data Structures *)

(** So far, we have only looked at propositions about natural numbers. However,
   we can define inductive predicates about any type of data. For example,
   suppose we would like to characterize lists of _even_ length. We can
   do that with the following definition.  *)

Inductive ev_list {X:Type} : list X -> Prop :=
  | el_nil : ev_list []
  | el_cc  : forall x y l, ev_list l -> ev_list (x :: y :: l).

Eval compute in ev_list [1;2;3;4].
Eval compute in el_nil.
Check @ev_list.
Check @el_cc.
Eval compute in el_cc 1 2 [1;2;3].
Eval compute in ev_list [1;2;3].
Eval compute in ev (length [1;2;3]).
(** Of course, this proposition is equivalent to just saying that the
length of the list is even. *)

Lemma ev_list__ev_length: forall X (l : list X), ev_list l -> ev (length l).
Proof.
    intros X l H. induction H.
    Case "el_nil". simpl. apply ev_0.
    Case "el_cc".  simpl.  apply ev_SS. apply IHev_list.
Qed.

(** However, because evidence for [ev] contains less information than
evidence for [ev_list], the converse direction must be stated very
carefully. *)

Lemma ev_length__ev_list: forall X n, ev n -> forall (l : list X), n = length l -> ev_list l.
Proof.
  intros X n H.
  induction H.
  Case "ev_0". intros l H. destruct l.
    SCase "[]". apply el_nil.
    SCase "x::l". inversion H.
  Case "ev_SS". intros l H2. destruct l.
    SCase "[]". inversion H2. destruct l.
    SCase "[x]". inversion H2.
    SCase "x :: x0 :: l". apply el_cc. apply IHev. inversion H2. reflexivity.
Qed.

(** **** Exercise: 4 stars (palindromes)  *)
(** A palindrome is a sequence that reads the same backwards as
    forwards.

    - Define an inductive proposition [pal] on [list X] that
      captures what it means to be a palindrome. (Hint: You'll need
      three cases.  Your definition should be based on the structure
      of the list; just having a single constructor
        c : forall l, l = rev l -> pal l
      may seem obvious, but will not work very well.)

    - Prove [pal_app_rev] that
       forall l, pal (l ++ rev l).
    - Prove [pal_rev] that
       forall l, pal l -> l = rev l.
*)
Inductive pal {X : Type} : list X -> Prop :=
|pal_nil: pal []
|pal_1: forall x, pal [x]
|pal_cc: forall x l, pal l -> pal (x :: (snoc l x)).

Eval compute in pal [1;2;3].
Theorem pal_app_rev : forall (X :Type) (l : list X),
pal (l ++ rev l).
Proof.
  intros.
  induction l.
  simpl. apply pal_nil.
  simpl. rewrite <- snoc_with_append.
  apply pal_cc.
  apply IHl.
Qed.
Theorem pal_rev : forall (X :Type) (l :list X),
pal l -> l = rev l.
Proof.
  intros.
  induction H.
  simpl. reflexivity.
  simpl. reflexivity.
  simpl. rewrite rev_snoc.
  simpl. apply f_equal.
  rewrite <- IHpal.
  reflexivity.
Qed.
(* FILL IN HERE *)
(** [] *)

(* Again, the converse direction is much more difficult, due to the
lack of evidence. *)

(** **** Exercise: 5 stars, optional (palindrome_converse)  *)
(** Using your definition of [pal] from the previous exercise, prove
    that
     forall l, l = rev l -> pal l.
*)

(* FILL IN HERE *)
(** [] *)

(* ####################################################### *)
(** ** Relations *)

(** A proposition parameterized by a number (such as [ev] or
    [beautiful]) can be thought of as a _property_ -- i.e., it defines
    a subset of [nat], namely those numbers for which the proposition
    is provable.  In the same way, a two-argument proposition can be
    thought of as a _relation_ -- i.e., it defines a set of pairs for
    which the proposition is provable. *)

Module LeModule.

(** One useful example is the "less than or equal to"
    relation on numbers. *)

(** The following definition should be fairly intuitive.  It
    says that there are two ways to give evidence that one number is
    less than or equal to another: either observe that they are the
    same number, or give evidence that the first is less than or equal
    to the predecessor of the second. *)

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

Notation "m <= n" := (le m n).

(** Proofs of facts about [<=] using the constructors [le_n] and
    [le_S] follow the same patterns as proofs about properties, like
    [ev] in chapter [Prop].  We can [apply] the constructors to prove [<=]
    goals (e.g., to show that [3<=3] or [3<=6]), and we can use
    tactics like [inversion] to extract information from [<=]
    hypotheses in the context (e.g., to prove that [(2 <= 1) -> 2+2=5].) *)

(** *** *)
(** Here are some sanity checks on the definition.  (Notice that,
    although these are the same kind of simple "unit tests" as we gave
    for the testing functions we wrote in the first few lectures, we
    must construct their proofs explicitly -- [simpl] and
    [reflexivity] don't do the job, because the proofs aren't just a
    matter of simplifying computations.) *)

Theorem test_le1 :
  3 <= 3.
Proof.
  (* WORKED IN CLASS *)
  apply le_n.  Qed.

Theorem test_le2 :
  3 <= 6.
Proof.
  (* WORKED IN CLASS *)
  apply le_S. apply le_S. apply le_S. apply le_n.  Qed.

Theorem test_le3 :
  (2 <= 1) -> 2 + 2 = 5.
Proof.
  (* WORKED IN CLASS *)
  intros H. inversion H. inversion H2.  Qed.

(** *** *)
(** The "strictly less than" relation [n < m] can now be defined
    in terms of [le]. *)

End LeModule.

Definition lt (n m:nat) := le (S n) m.

Notation "m < n" := (lt m n).

(** Here are a few more simple relations on numbers: *)

Inductive square_of : nat -> nat -> Prop :=
  sq : forall n:nat, square_of n (n * n).

Inductive next_nat : nat -> nat -> Prop :=
  | nn : forall n:nat, next_nat n (S n).

Inductive next_even : nat -> nat -> Prop :=
  | ne_1 : forall n, ev (S n) -> next_even n (S n)
  | ne_2 : forall n, ev (S (S n)) -> next_even n (S (S n)).

(** **** Exercise: 2 stars (total_relation)  *)
(** Define an inductive binary relation [total_relation] that holds
    between every pair of natural numbers. *)

(* FILL IN HERE *)
(** [] *)

(** **** Exercise: 2 stars (empty_relation)  *)
(** Define an inductive binary relation [empty_relation] (on numbers)
    that never holds. *)

(* FILL IN HERE *)
(** [] *)

(** **** Exercise: 2 stars, optional (le_exercises)  *)
(** Here are a number of facts about the [<=] and [<] relations that
    we are going to need later in the course.  The proofs make good
    practice exercises. *)

Lemma le_trans : forall m n o, m <= n -> n <= o -> m <= o.
Proof.
  intros m n o R1 R2.
  generalize dependent m.
  induction R2.
  intros m H. apply H.
  intros m0 H. apply IHR2 in H. apply le_S.
  apply H.
Qed.

Theorem O_le_n : forall n,
  0 <= n.
Proof.
  intros n.
  induction n.
  apply le_n.
  apply le_S. apply IHn.
Qed.

Theorem n_le_m__Sn_le_Sm : forall n m,
  n <= m -> S n <= S m.
Proof.
  intros n m H.
  induction H.
  apply le_n.
  apply le_S.
  apply IHle.
Qed.

Theorem Sn_le_Sm__n_le_m : forall n m,
  S n <= S m -> n <= m.
Proof.
  intros n m.
  generalize dependent n.
  induction m.
  intros n H.
  inversion H. apply le_n.
  inversion H1.
  intros n H.
  inversion H.
  rewrite <- H1. apply le_n.
  apply le_S. apply IHm.
  apply H1.
Qed.

Theorem le_plus_l : forall a b,
  a <= a + b.
Proof.
  intros a b.
  generalize dependent a.
  induction b.
  intros a.
  rewrite plus_0_r. apply le_n.
  intros a.
  rewrite <- plus_n_Sm.
  apply le_S.
  apply IHb.
Qed.

Theorem plus_lt : forall n1 n2 m,
  n1 + n2 < m ->
  n1 < m /\ n2 < m.
Proof.
  unfold lt.
  intros n1 n2 m H.
  split.
  apply le_trans with (n:=S (n1 + n2)).
  apply n_le_m__Sn_le_Sm.
  apply le_plus_l.
  apply H.
  apply le_trans with (n:=S (n1 + n2)).
  apply n_le_m__Sn_le_Sm.
  rewrite -> plus_comm.
  apply le_plus_l.
  apply H.
Qed.

Theorem lt_S : forall n m,
  n < m ->
  n < S m.
Proof.
  unfold lt.
  intros.
  induction H.
  apply le_S. apply le_n.
  apply le_S. apply IHle.
Qed.

Theorem ble_nat_true : forall n m,
  ble_nat n m = true -> n <= m.
Proof.
  intros n m H.
  generalize dependent m.
  induction n.
  intros m H.
  apply O_le_n.
  intros m H.
  induction m.
  inversion H.
  apply n_le_m__Sn_le_Sm.
  apply IHn.
  simpl in H.
  apply H.
Qed.

Theorem le_ble_nat : forall n m,
  n <= m ->
  ble_nat n m = true.
Proof.
  intros n m H.
  generalize dependent n.
  induction m.
  intros n H. inversion H. simpl. reflexivity.
  intros n H. induction n. simpl. reflexivity.
  simpl. apply IHm.
  apply Sn_le_Sm__n_le_m.
  apply H.
Qed.
  (* Hint: This may be easiest to prove by induction on [m]. *)

Theorem ble_nat_true_trans : forall n m o,
  ble_nat n m = true -> ble_nat m o = true -> ble_nat n o = true.
Proof.
  intros n m o H G.
  apply ble_nat_true in H.
  apply ble_nat_true in G.
  apply le_ble_nat.
  apply le_trans with (n:=m).
  apply H.
  apply G.
Qed.
  (* Hint: This theorem can be easily proved without using [induction]. *)

(** **** Exercise: 2 stars, optional (ble_nat_false)  *)
Theorem ble_nat_false : forall n m,
  ble_nat n m = false -> ~(n <= m).
Proof.
  intros.
  unfold not.
  intros.
  apply le_ble_nat in H0.
  rewrite H in H0.
  inversion H0.
Qed.
(** [] *)

(** **** Exercise: 3 stars (R_provability2)  *)
Module R.
(** We can define three-place relations, four-place relations,
    etc., in just the same way as binary relations.  For example,
    consider the following three-place relation on numbers: *)

Inductive R : nat -> nat -> nat -> Prop :=
   | c1 : R 0 0 0
   | c2 : forall m n o, R m n o -> R (S m) n (S o)
   | c3 : forall m n o, R m n o -> R m (S n) (S o)
   | c4 : forall m n o, R (S m) (S n) (S (S o)) -> R m n o
   | c5 : forall m n o, R m n o -> R n m o.

(** - Which of the following propositions are provable?
      - [R 1 1 2]
      - [R 2 2 6]

    - If we dropped constructor [c5] from the definition of [R],
      would the set of provable propositions change?  Briefly (1
      sentence) explain your answer.

    - If we dropped constructor [c4] from the definition of [R],
      would the set of provable propositions change?  Briefly (1
      sentence) explain your answer.

(* FILL IN HERE *)
[]
*)

(** **** Exercise: 3 stars, optional (R_fact)  *)
(** Relation [R] actually encodes a familiar function.  State and prove two
    theorems that formally connects the relation and the function.
    That is, if [R m n o] is true, what can we say about [m],
    [n], and [o], and vice versa?
*)

(* FILL IN HERE *)
(** [] *)

End R.

(** **** Exercise: 4 stars, advanced (subsequence)  *)
(** A list is a _subsequence_ of another list if all of the elements
    in the first list occur in the same order in the second list,
    possibly with some extra elements in between. For example,
    [1,2,3]
    is a subsequence of each of the lists
    [1,2,3]
    [1,1,1,2,2,3]
    [1,2,7,3]
    [5,6,1,9,9,2,7,3,8]
    but it is _not_ a subsequence of any of the lists
    [1,2]
    [1,3]
    [5,6,2,1,7,3,8]

    - Define an inductive proposition [subseq] on [list nat] that
      captures what it means to be a subsequence. (Hint: You'll need
      three cases.)

    - Prove [subseq_refl] that subsequence is reflexive, that is,
      any list is a subsequence of itself.

    - Prove [subseq_app] that for any lists [l1], [l2], and [l3],
      if [l1] is a subsequence of [l2], then [l1] is also a subsequence
      of [l2 ++ l3].

    - (Optional, harder) Prove [subseq_trans] that subsequence is
      transitive -- that is, if [l1] is a subsequence of [l2] and [l2]
      is a subsequence of [l3], then [l1] is a subsequence of [l3].
      Hint: choose your induction carefully!
*)

(* FILL IN HERE *)
(** [] *)

(** **** Exercise: 2 stars, optional (R_provability)  *)
(** Suppose we give Coq the following definition:
    Inductive R : nat -> list nat -> Prop :=
      | c1 : R 0 []
      | c2 : forall n l, R n l -> R (S n) (n :: l)
      | c3 : forall n l, R (S n) l -> R n l.
    Which of the following propositions are provable?

    - [R 2 [1,0]]
    - [R 1 [1,2,1,0]]
    - [R 6 [3,2,1,0]]
*)

(** [] *)

(* ##################################################### *)
(** * Programming with Propositions *)

(** As we have seen, a _proposition_ is a statement expressing a factual claim,
    like "two plus two equals four."  In Coq, propositions are written
    as expressions of type [Prop]. . *)

Check (2 + 2 = 4).
(* ===> 2 + 2 = 4 : Prop *)

Check (ble_nat 3 2 = false).
(* ===> ble_nat 3 2 = false : Prop *)

Check (beautiful 8).
(* ===> beautiful 8 : Prop *)

(** *** *)
(** Both provable and unprovable claims are perfectly good
    propositions.  Simply _being_ a proposition is one thing; being
    _provable_ is something else! *)

Check (2 + 2 = 5).
(* ===> 2 + 2 = 5 : Prop *)

Check (beautiful 4).
(* ===> beautiful 4 : Prop *)

(** Both [2 + 2 = 4] and [2 + 2 = 5] are legal expressions
    of type [Prop]. *)

(** *** *)
(** We've mainly seen one place that propositions can appear in Coq: in
    [Theorem] (and [Lemma] and [Example]) declarations. *)

Theorem plus_2_2_is_4 :
  2 + 2 = 4.
Proof. reflexivity.  Qed.

(** But they can be used in many other ways.  For example, we have also seen that
    we can give a name to a proposition using a [Definition], just as we have
    given names to expressions of other sorts. *)

Definition plus_fact : Prop  :=  2 + 2 = 4.
Check plus_fact.
(* ===> plus_fact : Prop *)

(** We can later use this name in any situation where a proposition is
    expected -- for example, as the claim in a [Theorem] declaration. *)

Theorem plus_fact_is_true :
  plus_fact.
Proof. reflexivity.  Qed.

(** *** *)
(** We've seen several ways of constructing propositions.

       - We can define a new proposition primitively using [Inductive].

       - Given two expressions [e1] and [e2] of the same type, we can
         form the proposition [e1 = e2], which states that their
         values are equal.

       - We can combine propositions using implication and
         quantification. *)
(** *** *)
(** We have also seen _parameterized propositions_, such as [even] and
    [beautiful]. *)

Check (even 4).
(* ===> even 4 : Prop *)
Check (even 3).
(* ===> even 3 : Prop *)
Check even.
(* ===> even : nat -> Prop *)

(** *** *)
(** The type of [even], i.e., [nat->Prop], can be pronounced in
    three equivalent ways: (1) "[even] is a _function_ from numbers to
    propositions," (2) "[even] is a _family_ of propositions, indexed
    by a number [n]," or (3) "[even] is a _property_ of numbers."  *)

(** Propositions -- including parameterized propositions -- are
    first-class citizens in Coq.  For example, we can define functions
    from numbers to propositions... *)

Definition between (n m o: nat) : Prop :=
  andb (ble_nat n o) (ble_nat o m) = true.

(** ... and then partially apply them: *)

Definition teen : nat->Prop := between 13 19.

(** We can even pass propositions -- including parameterized
    propositions -- as arguments to functions: *)

Definition true_for_zero (P:nat->Prop) : Prop :=
  P 0.

(** *** *)
(** Here are two more examples of passing parameterized propositions
    as arguments to a function.

    The first function, [true_for_all_numbers], takes a proposition
    [P] as argument and builds the proposition that [P] is true for
    all natural numbers. *)

Definition true_for_all_numbers (P:nat->Prop) : Prop :=
  forall n, P n.

(** The second, [preserved_by_S], takes [P] and builds the proposition
    that, if [P] is true for some natural number [n'], then it is also
    true by the successor of [n'] -- i.e. that [P] is _preserved by
    successor_: *)

Definition preserved_by_S (P:nat->Prop) : Prop :=
  forall n', P n' -> P (S n').

(** *** *)
(** Finally, we can put these ingredients together to define
a proposition stating that induction is valid for natural numbers: *)

Definition natural_number_induction_valid : Prop :=
  forall (P:nat->Prop),
    true_for_zero P ->
    preserved_by_S P ->
    true_for_all_numbers P.

(** **** Exercise: 3 stars (combine_odd_even)  *)
(** Complete the definition of the [combine_odd_even] function
    below. It takes as arguments two properties of numbers [Podd] and
    [Peven]. As its result, it should return a new property [P] such
    that [P n] is equivalent to [Podd n] when [n] is odd, and
    equivalent to [Peven n] otherwise. *)

Definition combine_odd_even (Podd Peven : nat -> Prop) : nat -> Prop :=
fun (n:nat) =>
  match oddb n with
      |true => Podd n
      |false => Peven n
  end.

(** To test your definition, see whether you can prove the following
    facts: *)

Theorem combine_odd_even_intro :
  forall (Podd Peven : nat -> Prop) (n : nat),
    (oddb n = true -> Podd n) ->
    (oddb n = false -> Peven n) ->
    combine_odd_even Podd Peven n.
Proof.
  intros Po Pe n H1 H2.
  unfold combine_odd_even.
  destruct (oddb n).
  apply H1. reflexivity.
  apply H2. reflexivity.
Qed.

Theorem combine_odd_even_elim_odd :
  forall (Podd Peven : nat -> Prop) (n : nat),
    combine_odd_even Podd Peven n ->
    oddb n = true ->
    Podd n.
Proof.
  intros Po Pe n H1 H2.
  unfold combine_odd_even in H1.
  rewrite -> H2 in H1.
  apply H1.
Qed.

Theorem combine_odd_even_elim_even :
  forall (Podd Peven : nat -> Prop) (n : nat),
    combine_odd_even Podd Peven n ->
    oddb n = false ->
    Peven n.
Proof.
  intros Po P3 n H1 H2.
  unfold combine_odd_even in H1.
  rewrite -> H2 in H1.
  apply H1.
Qed.

(** [] *)

(* ##################################################### *)
(** One more quick digression, for adventurous souls: if we can define
    parameterized propositions using [Definition], then can we also
    define them using [Fixpoint]?  Of course we can!  However, this
    kind of "recursive parameterization" doesn't correspond to
    anything very familiar from everyday mathematics.  The following
    exercise gives a slightly contrived example. *)

(** **** Exercise: 4 stars, optional (true_upto_n__true_everywhere)  *)
(** Define a recursive function
    [true_upto_n__true_everywhere] that makes
    [true_upto_n_example] work. *)

(*
Fixpoint true_upto_n__true_everywhere
(* FILL IN HERE *)

Example true_upto_n_example :
    (true_upto_n__true_everywhere 3 (fun n => even n))
  = (even 3 -> even 2 -> even 1 -> forall m : nat, even m).
Proof. reflexivity.  Qed.
*)
(** [] *)

(** $Date: 2014-12-31 11:17:56 -0500 (Wed, 31 Dec 2014) $ *)

author: ZefengZeng

repo: software-foundation


text:
Require Import List.
Require Import Setoid Morphisms QueryStructure.
Require Import AdditionalLemmas EnsembleListEquivalenceProperties.

Unset Implicit Arguments.

Add Parametric Morphism {A: Type} :
  (fun (P: A -> Prop) => exists x, P x)
    with signature (pointwise_relation A iff ==> iff)
      as exists_eq_iff_morphism.
Proof.
  intros * equiv;
  split; intro H; destruct H as [x0 H']; exists x0;
  apply equiv in H'; assumption.
Qed.

Add Parametric Morphism {A B: Type} :
  (fun comp seq => List.map comp seq)
    with signature (pointwise_relation A (@eq B) ==> eq ==> (@eq (list B)))
      as map_eq_morphism.
Proof.
  unfold pointwise_relation;
  intros * equiv seq;
  induction seq as [ | ? ? IH ]; simpl; [ | rewrite IH, equiv ]; trivial.
Qed.

Add Parametric Morphism {A B: Type} (seq: list A) :
  (fun comp => List.map comp seq)
    with signature (pointwise_relation A (@eq B) ==> (@eq (list B)))
      as map_eq_restricted_morphism.
Proof.
  intros.
  setoid_rewrite H; trivial.
Qed.

Add Parametric Morphism {A: Type} :
  (@List.filter A)
    with signature (pointwise_relation A (@eq bool) ==> @eq (list A) ==> @eq (list A))
      as filter_eq_morphism.
Proof.
  intros * equiv seq;
  unfold pointwise_relation in equiv;
  induction seq as [ | h t IH ];
  simpl;
  [ | rewrite equiv, IH ];
  trivial.
Qed.

Add Parametric Morphism {A: Type} (seq: list A) :
  (fun pred => @List.filter A pred seq)
    with signature (pointwise_relation A (@eq bool) ==> @eq (list A))
      as filter_eq_restricted_morphism.
Proof.
  intros * equiv;
  erewrite filter_eq_morphism; eauto.
Qed.

Require Import Permutation.

Add Parametric Morphism {A} :
  (@List.length A)
    with signature (@Permutation A ==> eq)
      as list_length_permutation_eq_morphism.
Proof.
  apply Permutation_length.
Qed.

Add Parametric Morphism {A B: Type} :
  (@List.map A B)
    with signature (pointwise_relation A (@eq B) ==> @Permutation A ==> @Permutation B)
      as map_permutation_morphism.
Proof.
  unfold pointwise_relation;
  intros * equiv seq1 seq2 is_perm.

  induction is_perm; simpl; rewrite ?equiv.

  constructor.
  constructor; eauto.
  erewrite map_eq_restricted_morphism; eauto; constructor.
  econstructor; eauto; cbv beta; erewrite map_eq_restricted_morphism; eauto; symmetry; eassumption.
Qed.

Ltac destruct_ifs :=
  repeat match goal with
           | [ |- context [ if ?A then _ else _ ] ] => destruct A
         end.

Add Parametric Morphism {A: Type} :
  (@List.filter A)
    with signature (pointwise_relation A (@eq bool) ==> @Permutation A ==> @Permutation A)
      as filter_permutation_morphism.
Proof.
  intros * equiv * is_perm.

  induction is_perm; simpl; rewrite ?equiv.

  constructor.
  destruct_ifs; try constructor;
  erewrite filter_eq_restricted_morphism; eauto; symmetry; eassumption.
  destruct_ifs; try constructor;
  erewrite filter_eq_restricted_morphism; eauto; symmetry; eassumption.
  econstructor. erewrite filter_eq_restricted_morphism; try (symmetry; eassumption).
  eauto. erewrite filter_eq_restricted_morphism; try (symmetry; eassumption).
  eassumption.
Qed.

Add Parametric Morphism {A: Type} :
  (@List.In A)
    with signature (@eq A ==> @Permutation A ==> iff)
      as in_permutation_morphism.
Proof.
  intros * is_perm.
  split; apply Permutation_in; intuition.
Qed.

Add Parametric Morphism {A: Type} :
  (@flatten A)
    with signature (@Permutation (list A) ==> @Permutation A)
      as flatten_permutation_morphism.
Proof.
  intros * is_perm.

  induction is_perm; simpl.

  constructor.
  apply Permutation_app_head; trivial.
  rewrite ?List.app_assoc; apply Permutation_app_tail; apply Permutation_app_comm.
  econstructor; eauto.
Qed.

Add Parametric Morphism {A B : Type} :
  (fun comp seq => @flatten B (@List.map A (list B) comp seq))
    with signature (pointwise_relation A (@Permutation B) ==> @eq (list A) ==> @Permutation B)
      as flatten_map_permutation_eq_permutation_morphism.
Proof.
  intros * equiv * seq.

  induction seq; simpl.
  constructor.
  apply Permutation_app; eauto.
Qed.

Add Parametric Morphism {A B : Type} :
  (@flat_map A B)
    with signature (pointwise_relation A (@Permutation B) ==> @eq (list A) ==> @Permutation B)
      as flatmap_permutation_eq_permutation_morphism.
Proof.
  intros.
  rewrite ?flat_map_flatten.
  apply flatten_map_permutation_eq_permutation_morphism; eauto.
Qed.

Add Parametric Morphism {A B: Type} :
  (fun comp seq => @flatten B (@List.map A (list B) comp seq))
    with signature (pointwise_relation A (@Permutation B) ==> @Permutation A ==> @Permutation B)
      as flatten_map_permutation_permutation_permutation_morphism.
Proof.
  unfold pointwise_relation;
  intros * equiv seq1 seq2 is_perm.

  induction is_perm; simpl.

  constructor.
  apply Permutation_app; eauto.

  rewrite ?List.app_assoc.
  apply Permutation_app.
  rewrite Permutation_app_comm;
    apply Permutation_app; apply equiv.

  apply flatten_map_permutation_eq_permutation_morphism; eauto.

  etransitivity;
    [ etransitivity; [ eauto | ] | eauto ].

  apply flatten_map_permutation_eq_permutation_morphism; try (symmetry; eauto).
Qed.

Add Parametric Morphism {A B : Type} :
  (@flat_map A B)
    with signature (pointwise_relation A (@Permutation B) ==> @Permutation A ==> @Permutation B)
      as flatmap_permutation_permutation_permutation_morphism.
Proof.
  intros.
  rewrite ?flat_map_flatten.
  apply flatten_map_permutation_permutation_permutation_morphism; eauto.
Qed.

Add Parametric Morphism {A B} :
  (@flat_map A B)
    with signature (pointwise_relation A eq ==> eq ==> eq)
      as flat_map_pointwiseeq_eq_eq_morphism_Proper.
Proof.
  intros * equiv ** seq.
  induction seq; simpl; [ | rewrite equiv, IHseq ]; reflexivity.
Qed.

Add Parametric Morphism {A B} :
  (flat_map (B := A * B))
    with signature (pointwise_relation A eq ==> eq ==> eq)
      as flat_map_pair_pointwiseeq_eq_eq_morphism.
Proof.
  intros * equiv ** seq.
  induction seq; simpl; [ | rewrite IHseq, equiv ]; reflexivity.
Qed.

Add Parametric Morphism {A: Type} :
  (@app A)
    with signature (@Permutation A ==> @Permutation A ==> @Permutation A)
      as app_permutation_permutation_permutation_morphism.
Proof.
  intros; apply Permutation_app; assumption.
Qed.

Add Parametric Morphism {A: Type} :
  (@rev A)
    with signature (@Permutation A ==> @Permutation A)
      as rev_permutation_permutation_morphism.
Proof.
  apply Permutation_rev'_Proper.
Qed.

Definition pointwise2_relation :=
  fun (A A': Type) {B : Type} (R : relation B) (f g : A -> A' -> B) =>
    forall a a', R (f a a') (g a a').

Add Parametric Morphism {A B: Type} :
  (@List.fold_right A B)
    with signature (@pointwise2_relation B A _ eq ==> eq ==> eq ==> eq)
      as fold_right_pointwise2eq_eq_eq_morphism.
Proof.
  intros * equiv default seq.
  induction seq; simpl.

  reflexivity.
  rewrite IHseq; apply equiv.
Qed.

Add Parametric Morphism {A B: Type} :
  (@List.fold_left A B)
    with signature (pointwise2_relation A B eq ==> eq ==> eq ==> eq)
      as fold_left_pointwise2eq_eq_eq_morphism.
Proof.
  intros.
  rewrite <- !fold_left_rev_right.
  setoid_rewrite H; reflexivity.
Qed.

Require Import Program Arith.
Require Import AdditionalPermutationLemmas.

Add Parametric Morphism {A: Type} (ens: A -> Prop) :
  (EnsembleListEquivalence ens)
    with signature (@Permutation A ==> @iff)
      as ensemble_list_equivalence_morphism.
Proof.
  firstorder; try eauto using NoDup_Permutation_rewrite.
  eapply Permutation_in; eauto; eapply H1; eauto.
  eapply Permutation_sym in H; eapply H1; eapply Permutation_in; eauto.
  apply Permutation_sym in H; try eauto using NoDup_Permutation_rewrite.
  apply Permutation_sym in H; eapply Permutation_in; eauto; eapply H1; eauto.
  eapply H1; eapply Permutation_in; eauto.
Qed.

Add Morphism
    (decides)
    with signature (eq ==> iff ==> iff)
      as decide_eq_iff_iff_morphism.
Proof.
  unfold decides; intros b p1 p2 equiv.
  destruct b; simpl; intuition.
Qed.

author: JasonGross

repo: adt-synthesis


text:
Require Import Coq.Strings.String Coq.Strings.Ascii.
Require Import Coq.Classes.Morphisms.
Require Import Fiat.Parsers.Reflective.Syntax.
Require Import Fiat.Parsers.Reflective.Semantics.
Require Import Fiat.Parsers.Reflective.ParserSyntax.
Require Import Fiat.Parsers.Reflective.ParserSemantics.
Require Import Fiat.Parsers.Reflective.SemanticsOptimized.
Require Import Fiat.Parsers.Reflective.ParserSemanticsOptimized.
Require Import Fiat.Parsers.Reflective.ParserSoundness.
Require Import Fiat.Parsers.Reflective.PartialUnfold.
Require Import Fiat.Parsers.Reflective.ParserPartialUnfold.
Set Implicit Arguments.

Module opt.
  Section polypnormalize.
    Context (is_valid_nonterminal : list nat -> nat -> bool)
            (strlen : nat)
            (char_at_matches_interp : nat -> Reflective.RCharExpr Ascii.ascii -> bool)
            (split_string_for_production : nat * (nat * nat) -> nat -> nat -> list nat).

    Let interp {T} := opt.interp_has_parse_term (T := T) is_valid_nonterminal strlen char_at_matches_interp split_string_for_production.

    Lemma polypnormalize_correct {T} (term : polyhas_parse_term T)
      : ParserSyntaxEquivalence.has_parse_term_equiv
          nil
          (term interp_TypeCode) (term (normalized_of interp_TypeCode))
        -> interp (term _) = interp (polypnormalize term _).
    Proof.
      apply polypnormalize_correct; assumption.
    Qed.
  End polypnormalize.
End opt.

repo: slow-coq-examples


text:
(** This file implements a tactical [delaying tac] and a tactic
  [delay], which function in the following way: [tac] is able to
  invoke [delay] to solve any subgoal. Assuming the subgoal can be
  typed in the context in which [delaying tac] was invoked, the
  [delay] tactic will succeed, and the subgoal will instead become a
  subgoal of the encolosing invocation of [delaying tac].

  To see why this is useful, consider the way [eauto] works. Applying
  an [eauto] hint is only considered successful when the generated
  subgoal can themselves be solved by [eauto]. Otherwise, [eauto]
  backtracks and another hint is used. If no hint can be used to solve
  the goal completely, then no progress is made.

  While this behavior is usually appropriate, this means [eauto]
  cannot be used as a base for tactics which make as much progress as
  possible, then let the user (or another tactic in a sequence) solve
  the remaining subgoals. With the tactics defined below, this can be
  accomplished by registering an external hint making use of [delay]
  for strategic subgoals, and invoking [delaying eauto].

  Additionally, the variant [delaying_conjunction] bundles all of the
  subgoals solved by [delay] in a single conjunction of the form
  [P1 /\ ... /\ Pn /\ True]. This is useful as it provides a uniform
  interface when reifying the effect of a tactic. *)

(** * The [delayed]/[delay] tactics *)

Module Delay.
  (** The [delaying] tactical and the [delay] tactic communicate
    through the use of existential variables. Specifically, [delaying]
    introduces a so-called "open conjunction" to the context. The open
    conjunction starts as a hypothesis of type [?P], and remains of
    the form [P1 /\ ... /\ Pn /\ ?Q] throughout. Each invocation of
    [delay] unifies [?Q] with a new node [Pi /\ ?Q']. [Pi] will be of
    the form [forall x1 .. xn, delayed_goal G], where [G] is the
    original goal and the [xi]s are the new variables which were
    introduced after the open conjunction was created. *)

  Ltac use_conjunction H :=
    lazymatch type of H with
      | ?A /\ ?B =>
        use_conjunction (@proj2 A B H)
      | _ =>
        eapply (proj1 H)
    end.

  (** As much as possible, our open conjunction should remain hidden
    from the user's point of view. To avoid interfering with random
    tactics such as [eassumption], we wrap it in the following record
    type. *)

  Record open_conjunction (P: Prop) :=
    {
      open_conjunction_proj: P
    }.

  (** The evar can only be instantiated to refer to variables that
    existed at the point where the evar is spawned. As a consequence,
    in order to use it, we must first get rid of all of the new
    variables, which the goal potentially depends on. We do this by
    reverting the context one variable at a time from the bottom up,
    until we hit our [open_conjunction]. *)

  Ltac revert_until_conjunction Hdelayed :=
    match goal with
      | |- open_conjunction _ -> _ =>
        intro Hdelayed
      | H : _ |- _ =>
        revert H;
        revert_until_conjunction Hdelayed
    end.

  (** To make sure this operation is reversible, we first wrap the
    goal using the following marker. *)

  Definition delayed_goal (P: Prop) := P.

  (** In some contexts, we actually want a nested saved goal to be
    split up further instead. The following marker does that. *)

  Definition unpack (P: Prop) := P.

  (** Once we're done, we've packaged all of the goals we solved using
    [use_conjunction] into a single hypothesis. We can use the
    following tactic to split up that conjunction into individual
    subgoals again.

    Although we expect the conjunctions produced by [use_conjunction]
    to be terminated by [True] and this should be regarded as the
    canonical format, when the last conjunct is a non-[True]
    proposition we consider it as an additional subgoal. Likewise we
    don't require the conclusions to be wrapped in [delayed_goal].
    This allows for some flexibility when dealing with manually
    written goals. *)

  Ltac split_conjunction :=
    let handle_subgoal :=
      intros;
      match goal with
        | |- delayed_goal _ => red
        | |- unpack _ => red; split_conjunction
        | |- _ => idtac
      end in
    match goal with
      | |- _ /\ _ => split; [handle_subgoal | split_conjunction]
      | |- _ => exact I
      | |- _ => handle_subgoal
    end.

  (** Now we can defined [delayed], [delayed_conjunction] and [delay]. *)

  Ltac delay :=
    idtac;
    lazymatch goal with
      | _ : open_conjunction _ |- ?G =>
        change (delayed_goal G);
        let Hdelayed := fresh "Hdelayed" in
        revert_until_conjunction Hdelayed;
        use_conjunction (open_conjunction_proj _ Hdelayed)
      | _ =>
        fail "delay can only be used under the 'delayed' tactical"
    end.

  Ltac delayed_conjunction tac :=
    let Pv := fresh in evar (Pv: Prop);
    let P := eval red in Pv in clear Pv;
    let Hdelayed := fresh "Hdelayed" in
    cut (open_conjunction P);
    [ intro Hdelayed; tac; clear Hdelayed |
      eapply Build_open_conjunction ].

  Ltac delayed tac :=
    delayed_conjunction tac;
    [ .. | split_conjunction ].

  Ltac undelay :=
    lazymatch goal with
      | Hdelayed : open_conjunction _ |- _ =>
        clear Hdelayed
    end.

  Ltac nondelayed tac :=
    undelay; tac.
End Delay.

Tactic Notation "delayed" tactic1(tac) :=
  Delay.delayed tac.

Tactic Notation "nondelayed" tactic1(tac) :=
  Delay.nondelayed tac.

Tactic Notation "delayed_conjunction" tactic1(tac) :=
  Delay.delayed_conjunction tac.

Tactic Notation "delay" := Delay.delay.

(** * Hints *)

(** We hook [delay] into [eauto] in two different ways: subgoals
  intended to be delayed can be marked with the wrapper below.
  Alternately, one can use the [delay] hint database, which provides a
  low-priority delay rule. *)

Definition delay (P: Prop) := P.

Hint Extern 0 (delay _) => delay.

Hint Extern 100 => delay : delay.

(** This typeclass wrapper is convenient for performing a nested
  search outside of a potential "delayed" context. *)

Class NonDelayed (P: Prop) :=
  nondelayed : P.

Hint Extern 1 (NonDelayed _) =>
  red; try Delay.undelay : typeclass_instances.

(** * Example: reifying [eapply] *)

(** To demonstrate how [delayed_conjunction] can be used to reify a
  tactic into a typeclass, we define the [EApply] typeclass. An
  instance of [EApply HT P Q] expresses that if [H] is a hypothesis of
  type [HT], then invoking [eapply H] on a goal of type [Q] will
  generate the subgoal conjunction [P]. *)

Class EApply (HT P Q: Prop) :=
  eapply : HT -> P -> Q.

Hint Extern 1 (EApply ?HT _ _) =>
  let H := fresh in
  let HP := fresh "HP" in
    intros H HP;
    delayed_conjunction solve [eapply H; delay];
    eexact HP :
  typeclass_instances.

author: DeepSpec


text:
Require Export imports.
Require Export AExp.
Require Export BExp.

Inductive com :=
| Skip : com
| Assign : vname -> aexpr -> com
| Seq : com -> com -> com
| If : bexpr -> com -> com -> com
| While : bexpr -> com -> com.

author: lukaszcz

repo: COQ-IMP

save_path: github-repos/coq/lukaszcz-COQ-IMP