Module Partiality

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.


Generated by coq2html