Partiality.v

From Coq Require Import Arith ZArith Psatz Bool String List.
From CDF Require Import Sequences IMP.

(** * 6.  Sémantiques de la divergence, deuxième partie *)

(** ** 6.5.  La monade de partialité *)

(** Le type [delay A] représente les calculs qui produisent un
    résultat de type [A] s'ils terminent, mais peuvent aussi
    ne pas terminer. *)

CoInductive delay (A: Type) : Type :=
  | now: A -> delay A
  | later: delay A -> delay A.

Arguments now [A].
Arguments later [A].

(** Le calcul de type [A] qui diverge toujours. *)

CoFixpoint omega (A: Type) : delay A := later (omega A).

(** Quelques définitions techniques pour montrer des égalités entre calculs. *)

Lemma u_delay:
  forall {A: Type} (x: delay A),
  x = match x with now v => now v | later y => later y end.
Proof. destruct x; auto. Qed.

Ltac unroll_delay X := rewrite (u_delay X); simpl.

Ltac samedelay :=
  match goal with
  [ |- ?X = ?Y ] => rewrite (u_delay X); simpl; auto
  end.

(** La terminaison sur une valeur [v] est définie par un prédicat inductif
    [terminates x v].
    La divergence est définie par un prédicat coinductif [diverges x]. *)

Inductive terminates {A: Type} : delay A -> A -> Prop :=
  | terminates_now:   forall v, terminates (now v) v
  | terminates_later: forall x v, terminates x v -> terminates (later x) v.

CoInductive diverges {A: Type} : delay A -> Prop :=
  | diverges_later: forall x, diverges x -> diverges (later x).

Lemma terminates_unique: forall (A: Type) (x: delay A) (v1 v2: A),
  terminates x v1 -> terminates x v2 -> v1 = v2.
Proof.
  intros until v2; intros T; revert x v1 T v2. induction 1; intros.
- inversion H; subst; auto.
- inversion H; subst; auto.
Qed.

Lemma terminates_diverges_excl: forall (A: Type) (x: delay A) (v: A),
  terminates x v -> diverges x -> False.
Proof.
  induction 1; intros D; inversion D; auto.
Qed.

(** Exemple d'utilisation: le reste de la division euclidienne. *)

CoFixpoint remainder (a b: nat) : delay nat :=
  if a <? b then now a else later (remainder (a - b) b).

Lemma remainder_terminates:
  forall a b, b > 0 -> 
  exists q r, terminates (remainder a b) r /\ r < b /\ a = b * q + r.
Proof.
  induction a using (well_founded_ind lt_wf). intros.
  unroll_delay (remainder a b). destruct (Nat.ltb_spec a b).
- exists 0, a. split. constructor. split. auto. lia. 
- assert (LT: a - b < a) by lia. 
  destruct (H _ LT b H0) as (q & r & P & Q & R).
  exists (S q), r. split. constructor; auto. split. auto. lia.
Qed.

Lemma remainder_diverges:
  forall a, diverges (remainder a 0).
Proof.
  cofix CIH; intros a. unroll_delay (remainder a 0). constructor. apply CIH.
Qed.

(** Équiterminaison de deux calculs. *)

Section EQUITERMINATION.

Context {A: Type}.

CoInductive equi: delay A -> delay A -> Prop :=
  | equi_terminates: forall x y v, terminates x v -> terminates y v -> equi x y
  | equi_later: forall x y, equi x y -> equi (later x) (later y).

Notation "x == y" := (equi x y) (at level 70, no associativity).

Lemma equi_refl: forall x, x == x.
Proof.
  cofix COINDHYP; intros; destruct x.
- apply equi_terminates with a; constructor.
- apply equi_later. apply COINDHYP.
Qed.

Lemma equi_refl': forall x y, x = y -> x == y.
Proof.
  intros; subst; apply equi_refl.
Qed.

Lemma equi_sym: forall x y, x == y -> y == x.
Proof.
  cofix COINDHYP; intros x y E; inversion E; subst.
- apply equi_terminates with v; auto.
- apply equi_later; apply COINDHYP; auto.
Qed.

Lemma terminates_equi: 
  forall x v, terminates x v -> forall y, x == y -> terminates y v.
Proof.
  induction 1; intros y E; inversion E; subst.
- inversion H; auto.
- inversion H0; subst. 
  assert (v0 = v) by (eapply terminates_unique; eauto). subst v0; auto.
- constructor; eauto.
Qed.

Lemma equi_trans: forall x y z, x == y -> y == z -> x == z.
Proof.
  cofix COINDHYP; intros x y z E1 E2; inversion E1; subst.
- apply equi_terminates with v. auto. apply terminates_equi with y; auto.
- inversion E2; subst.
+ inversion H0; subst. apply equi_terminates with v; auto. constructor. 
  apply terminates_equi with y0; auto using equi_sym.
+ constructor. apply COINDHYP with y0; auto.
Qed.

Lemma eq_later: forall x, later x == x.
Proof.
  cofix COINDHYP; intros x. destruct x. 
- apply equi_terminates with a; repeat constructor.
- apply equi_later. apply COINDHYP.
Qed. 

Lemma diverges_equi: forall x y, x == y -> diverges x -> diverges y.
Proof.
  cofix COINDHYP; intros. inversion H; subst.
- elim (terminates_diverges_excl A x v); auto.
- inversion H0; subst. constructor. eauto.
Qed. 

(** La bisimulation faible.  C'est une autre présentation de l'équiterminaison,
    avec des constructeurs [bisim_left] et [bisim_right] qui permettent
    de "sauter" un constructeur [later] d'un côté mais pas de l'autre.
    Ceci facilite certaines démonstrations.  Cependant, il faut empêcher
    d'appliquer [bisim_left] ou [bisim_right] une infinité de fois,
    car cela rendrait bisimilaires [now v] et [bottom].  L'argument de type
    [nat] permet de limiter le nombre d'applications consécutives
    des règles [bisim_left] et [bisim_right].  Il est remis à une valeur
    arbitrairement élevée lorsque [bisim_both] est appliqué. *)

CoInductive bisim: nat -> delay A -> delay A -> Prop :=
  | bisim_now: forall n v,
      bisim n (now v) (now v)
  | bisim_both: forall m n x y,
      bisim m x y -> bisim n (later x) (later y)
  | bisim_left: forall n x y,
      bisim n x y -> bisim (S n) (later x) y
  | bisim_right: forall n x y,
      bisim n x y -> bisim (S n) x (later y).

Lemma bisim_inv: forall n x y,
  bisim n x y ->
     (exists v, terminates x v /\ terminates y v)
  \/ (exists n' x' y', x = later x' /\ y = later y' /\ bisim n' x' y').
Proof.
  induction n using lt_wf_ind.
  intros x y B; inversion B; subst.
- left; exists v; split; constructor.
- right; exists m, x0, y0; auto.
- edestruct (H n0) as [(v & T1 & T2) | (n' & x' & y' & E1 & E2 & B')].
  lia. eauto.
  + left; exists v; auto using terminates_later.
  + right. exists (S n'), (later x'), y'; intuition auto.
    congruence. apply bisim_left; auto.
- edestruct (H n0) as [(v & T1 & T2) | (n' & x' & y' & E1 & E2 & B')].
  lia. eauto.
  + left; exists v; auto using terminates_later.
  + right. exists (S n'), x', (later y'); intuition auto.
    congruence. apply bisim_right; auto.
Qed.

Lemma bisim_equi: forall n x y,
  bisim n x y -> x == y.
Proof.
  cofix CIH; intros.
  destruct (bisim_inv _ _ _ H)
  as [(v & T1 & T2) | (n' & x' & y' & E1 & E2 & B')].
- apply equi_terminates with v; auto.
- subst. constructor. eauto.
Qed.

End EQUITERMINATION.

Notation "x == y" := (equi x y) (at level 70, no associativity).

(** La structure de monade. *)

Definition ret := now.

CoFixpoint bind {A B: Type} (x: delay A) (f: A -> delay B) : delay B :=
  match x with
  | now v => later (f v)
  | later y => later (bind y f)
  end.

Remark bind_now: forall (A B: Type) (v: A) (f: A -> delay B),
  bind (now v) f = later (f v).
Proof. intros; samedelay. Qed.

Remark bind_later: forall (A B: Type) (x: delay A) (f: A -> delay B),
  bind (later x) f = later (bind x f).
Proof. intros; samedelay. Qed.

(** Les trois lois monadiques sont vraies à équiterminaison près. *)

Lemma mon_law_1: forall (A B: Type) (v: A) (f: A -> delay B),
  bind (now v) f == f v.
Proof. 
  intros. rewrite bind_now. apply eq_later.
Qed.

Lemma mon_law_2: forall (A: Type) (m: delay A), 
  bind m (@ret A) == m.
Proof.
  cofix CIH; intros. destruct m.
- rewrite bind_now. apply eq_later. 
- rewrite bind_later. constructor. apply CIH.
Qed.

Lemma mon_law_3: forall (A B C: Type) (m: delay A) (f: A -> delay B) (g: B -> delay C),
  bind (bind m f) g == bind m (fun x => bind (f x) g).
Proof.
  cofix CIH. intros; destruct m.
- rewrite ! bind_now, bind_later. apply equi_refl.
- rewrite ! bind_later. constructor. apply CIH.
Qed.

(** [bind] est compatible avec l'équiterminaison [==]. *)

Lemma bind_terminates_l:
  forall (A: Type) (m: delay A) (v: A), terminates m v ->
  forall (B: Type) (f: A -> delay B), bind m f == f v.
Proof.
  induction 1; intros.
- apply mon_law_1.
- rewrite bind_later. eapply equi_trans. apply eq_later. apply IHterminates. 
Qed.

Lemma bind_context:
  forall (A B: Type) (m1 m2: delay A) (f1 f2: A -> delay B),
  m1 == m2 ->
  (forall v, f1 v == f2 v) ->
  bind m1 f1 == bind m2 f2.
Proof.
  cofix CIH; intros. inversion H; subst.
- apply equi_trans with (f1 v). apply bind_terminates_l; auto.
  apply equi_trans with (f2 v). auto.
  apply equi_sym. apply bind_terminates_l; auto.
- rewrite ! bind_later. constructor. apply CIH; auto.
Qed.

(** ** 6.6.  Le métalangage monadique *)

(** Voici la syntaxe abstraite (coinductive) qui représente des calculs
    dans la monade de partialité.  *)

CoInductive mon (A: Type): Type :=
  | Ret: A -> mon A
  | Later: mon A -> mon A
  | Bind: forall {B: Type}, mon B -> (B -> mon A) -> mon A.

Arguments Ret [A].
Arguments Later [A].
Arguments Bind [A B].

Lemma u_mon:
  forall {A: Type} (x: mon A),
  x = match x with Ret v => Ret v | Bind y f => Bind y f | Later m => Later m end.
Proof. destruct x; auto. Qed.

(** La sémantique d'un arbre de syntaxe abstraite (de type [mon A])
    est définie par traduction vers le calcul (de type [delay A])
    qu'il dénote. *)

CoFixpoint run {A: Type} (m: mon A) : delay A :=
  match m with
  | Ret v => now v
  | Later m => later (run m)
  | Bind (Ret v) f => later (run (f v))
  | Bind (Later m) f => later (run (Bind m f))
  | Bind (Bind m f) g => later (run (Bind m (fun x => Bind (f x) g)))
  end.

Lemma run_Ret: forall (A: Type) (v: A), run (Ret v) = now v.
Proof. intros; samedelay. Qed.

Lemma run_Later: forall (A: Type) (m: mon A), run (Later m) = later (run m).
Proof. intros; samedelay. Qed.

Lemma run_Bind_Ret: forall (A B: Type) (v: A) (f: A -> mon B),
    run (Bind (Ret v) f) = later (run (f v)).
Proof. intros; samedelay. Qed.

Lemma run_Bind_Later: forall (A B: Type) (m: mon A) (f: A -> mon B),
    run (Bind (Later m) f) = later (run (Bind m f)).
Proof. intros; samedelay. Qed.

Lemma run_Bind_Bind: forall (A B C: Type) (m: mon A) (f: A -> mon B) (g: B -> mon C),
    run (Bind (Bind m f) g) = later (run (Bind m (fun x => Bind (f x) g))).
Proof. intros; samedelay. Qed.

(** Pour certaines démonstrations, on utilise des continuations, que l'on peut
    aussi voir comme des contextes, et qui se composent d'une liste de
    fonctions [A -> mon B] qui peuvent se composer. *)

Inductive cont: Type -> Type -> Type :=
  | K0: forall (A: Type), cont A A
  | Kbind: forall {A B C: Type} (f: A -> mon B) (k: cont B C), cont A C.

Fixpoint insert_cont {A B: Type} (k: cont A B): 
    forall {C: Type}, (B -> mon C) -> (A -> mon C) :=
  match k in cont A B 
  return forall {C: Type}, (B -> mon C) -> (A -> mon C) with
  | K0 A => fun C g => g
  | Kbind f k => fun D g a => Bind (f a) (insert_cont k g)
  end.

(** Les trois lois monadiques.  *)

Lemma Mon_law_1: forall (A B: Type) (v: A) (f: A -> mon B),
  run (Bind (Ret v) f) == run (f v).
Proof. 
  intros. rewrite run_Bind_Ret; apply eq_later. 
Qed.

Lemma Mon_law_3: forall (A B C: Type) (m: mon A) (f: A -> mon B) (g: B -> mon C),
  run (Bind (Bind m f) g) == run (Bind m (fun x => Bind (f x) g)).
Proof.
  intros. rewrite run_Bind_Bind; apply eq_later.
Qed.

(** La deuxième loi monadique est particulièrement difficile à démontrer.
    On utilise la bisimulation en lien avec la relation ci-dessous. *)

Inductive eta_match: forall {A: Type}, nat -> mon A -> mon A -> Prop :=
| eta_match_1: forall {A: Type} (m: mon A),
    eta_match 1%nat (Bind m (@Ret _)) m
| eta_match_2: forall {A B C: Type} (m: mon A) (k: cont A B) (g: B -> mon C),
    eta_match 0%nat (Bind m (insert_cont k (fun x => Bind (g x) (@Ret _))))
                    (Bind m (insert_cont k g)).

Lemma Mon_law_2_aux:
  forall (A: Type) n (x y: mon A),
  eta_match n x y -> bisim n (run x) (run y).
Proof.
  cofix CIH; destruct 1.  
  - destruct m.
    + rewrite run_Bind_Ret, run_Ret.
      apply bisim_left. apply bisim_now.
    + rewrite run_Bind_Later, run_Later.
      eapply bisim_both. apply CIH. apply eta_match_1.
    + rewrite run_Bind_Bind.
      apply bisim_left. apply CIH.
      apply eta_match_2 with (k := K0 _).
  - destruct m.
    + rewrite ! run_Bind_Ret. destruct k; simpl.
      * eapply bisim_both. apply CIH. apply eta_match_1. 
      * eapply bisim_both. apply CIH. apply eta_match_2.
    + rewrite ! run_Bind_Later.
      eapply bisim_both. apply CIH. apply eta_match_2.
    + rewrite ! run_Bind_Bind.
      eapply bisim_both. apply CIH.
      apply eta_match_2 with (k := Kbind m0 k).
Qed.

Lemma Mon_law_2:
  forall (A: Type) (m: mon A), run (Bind m (@Ret A)) == run m.
Proof.
  intros. eapply bisim_equi. apply Mon_law_2_aux. apply eta_match_1.
Qed.

(** Il s'ensuit que la dénotation d'un [Bind] est le [bind] des dénotations. *)

Lemma run_Bind_aux:
  forall (A B C: Type) (m: mon A) (k: cont A B) (f: B -> mon C),
  run (Bind m (insert_cont k f)) ==
  bind (run (Bind m (insert_cont k (@Ret _)))) (fun x => run (f x)).
Proof.
  cofix CIH; intros.
  destruct m.
  - rewrite ! run_Bind_Ret. destruct k; cbn.
    + rewrite run_Ret, bind_later, bind_now.
      constructor. apply equi_sym; apply eq_later.
    + rewrite bind_later. apply equi_later. apply CIH.
  - rewrite ! run_Bind_Later, bind_later.
    apply equi_later. apply CIH.
  - rewrite ! run_Bind_Bind, bind_later. 
    apply equi_later. apply CIH with (k := Kbind m0 k).
Qed.

Theorem run_Bind:
  forall (A B: Type) (m: mon A) (f: A -> mon B),
  run (Bind m f) == bind (run m) (fun x => run (f x)).
Proof.
  intros. 
  change (Bind m f) with (Bind m (insert_cont (K0 _) f)).
  eapply equi_trans. apply run_Bind_aux. apply bind_context. 
  apply Mon_law_2.
  intros; apply equi_refl.
Qed.

(** ** 6.7.  Application: un interpréteur / une sémantique dénotationnelle pour IMP *)

CoFixpoint cinterp (c: com) (s: store) : mon store :=
  match c with
  | SKIP => Ret s
  | ASSIGN x a => Ret (update x (aeval a s) s)
  | SEQ c1 c2 => Bind (cinterp c1 s) (cinterp c2)
  | IFTHENELSE b c1 c2 =>
      Later (cinterp (if beval b s then c1 else c2) s)
  | WHILE b c =>
      if beval b s then Bind (cinterp c s) (cinterp (WHILE b c))
                   else Ret s
  end.

(** La dénotation d'une commande est l'exécution de son interprétation. *)

Definition denot (c: com) (s: store) : delay store := run (cinterp c s).

(** Les équations de la sémantique dénotationnelle d'IMP sont vérifiées. *)

Lemma denot_skip: forall s,
  denot SKIP s == now s.
Proof.
  intros. unroll_delay (denot SKIP s). apply equi_refl.
Qed.

Lemma denot_assign: forall x a s,
  denot (ASSIGN x a) s == now (update x (aeval a s) s).
Proof.
  intros. unroll_delay (denot (ASSIGN x a) s). apply equi_refl.
Qed.

Lemma denot_seq: forall c1 c2 s,
  denot (SEQ c1 c2) s == bind (denot c1 s) (denot c2).
Proof.
  unfold denot; intros. rewrite (u_mon (cinterp (c1;;c2) s)); cbn.
  apply run_Bind.
Qed.

Lemma denot_ifthenelse: forall b c1 c2 s,
  denot (IFTHENELSE b c1 c2) s == if beval b s then denot c1 s else denot c2 s.
Proof.
  unfold denot; intros. rewrite (u_mon (cinterp (IFTHENELSE b c1 c2) s)); cbn.
  rewrite run_Later. destruct (beval b s); apply eq_later.
Qed.

Lemma denot_while: forall b c s,
  denot (WHILE b c) s ==
  if beval b s then bind (denot c s) (denot (WHILE b c)) else now s.
Proof.
  unfold denot; intros. rewrite (u_mon (cinterp (WHILE b c) s)); cbn.
  destruct (beval b s).
- apply run_Bind.
- rewrite run_Ret. apply equi_refl.
Qed.