predicate lifting 使ってモナディックな計算についてホーア論理的な形式で命題記述できるようにする仕組みを Maybe モナドと State モナドに具体化したやつ。

mpl_state.v

Set Implicit Arguments.
Unset Strict Implicit.

Require Import Setoids.Setoid Morphisms.
Generalizable All Variables.

Class Setoid :=
  {
    carrier: Type;
    equal: carrier -> carrier -> Prop;
    prf_Setoid: Equivalence equal
  }.
Coercion carrier: Setoid >-> Sortclass.
Coercion prf_Setoid: Setoid >-> Equivalence.
Existing Instance prf_Setoid.
Notation "(== :> X )" := (equal (Setoid:=X)).
Notation "(==)" := (==:>_) (only parsing).
Notation "x == y :> X" := (equal (Setoid:=X) x y) (at level 90, no associativity).
Notation "x == y" := (equal x y) (at level 90, no associativity, only parsing).

Class Map (X Y: Setoid) :=
  {
    map: X -> Y;
    substitute: Proper ((==) ==> (==)) map
  }.
Coercion map: Map >-> Funclass.
Existing Instance substitute.

Instance Map_setoid (X Y: Setoid): Setoid :=
  {
    carrier := Map X Y;
    equal f g := forall x, f x == g x
  }.
Proof.
  split.
  - intros f x; reflexivity.
  - intros f g Heq x; symmetry; apply Heq.
  - intros f g h H H' x; transitivity (g x); [apply H | apply H'].
Defined.

Instance Map_comp {X Y Z: Setoid}(f: Map X Y)(g: Map Y Z): Map X Z :=
  {
    map x := g (f x)
  }.
Proof.
  intros x y Heq; repeat apply substitute; auto.
Defined.

Instance Map_id (X: Setoid): Map X X :=
  {
    map x := x
  }.
Proof.
  intros x y Heq; auto.
Defined.

Class Category :=
  {
    obj: Type;
    hom: obj -> obj -> Setoid;
    comp: forall {X Y Z: obj}, hom X Y -> hom Y Z -> hom X Z;
    id: forall (X: obj), hom X X;

    comp_subst:
      forall (X Y Z: obj)(f f': hom X Y)(g g': hom Y Z),
        f == f' -> g == g' -> comp f g == comp f' g';

    comp_assoc:
      forall {X Y Z W: obj}(f: hom X Y)(g: hom Y Z)(h: hom Z W),
        comp f (comp g h) == comp (comp f g) h;

    comp_id_dom:
      forall {X Y: obj}(f: hom X Y),
        comp (id X) f == f;

    comp_id_cod:
      forall {X Y: obj}(f: hom X Y),
        comp f (id Y) == f
  }.
Coercion obj: Category >-> Sortclass.
Coercion hom: Category >-> Funclass.
Notation "g \o{ C } f" := (comp (Category:=C) f g) (at level 60, right associativity).
Notation "g \o f" := (g \o{_} f) (at level 60, right associativity).
Notation "'Id' X" := (id X) (at level 60, right associativity).

Class Kleisli (C: Category)(T: C -> C) :=
  {
    pure: forall {X: C}, C X (T X);
    bind: forall {X Y: C}, C X (T Y) -> C (T X) (T Y);

    bind_pure:
      forall {X: C},
        bind (pure (X:=X)) == id (T X);

    pure_bind:
      forall {X Y: C}(f: hom X (T Y)),
        bind f \o pure == f;

    bind_bind:
      forall {X Y Z: C}(f: hom X (T Y))(g: hom Y (T Z)),
        bind g \o bind f == bind (bind g \o f)
  }.


Class PartialOrder {A: Type}(eq: relation A){equiv: Equivalence eq}(R: relation A) :=
  {
    PartialOrder_Reflexive: Reflexive R;
    PartialOrder_Transitive: Transitive R;
    PartialOrder_Antisymmetric: Antisymmetric A eq R
  }.
Existing Instance PartialOrder_Reflexive.
Existing Instance PartialOrder_Transitive.
Existing Instance PartialOrder_Antisymmetric.
Arguments PartialOrder A eq {equiv} R: clear implicits.
Class Poset :=
  {
    poset_setoid: Setoid;
    poset_pord: relation poset_setoid;
    poset_pord_subst: Proper ((==) ==> (==) ==> (fun P Q: Prop => P -> Q))  poset_pord;
    poset_pord_partialorder: PartialOrder poset_setoid (==:> poset_setoid) poset_pord
  }.
Notation "(<=p)" := poset_pord.
Infix "<=p" := poset_pord (at level 80, no associativity).
Coercion poset_setoid: Poset >-> Setoid.
Existing Instance poset_setoid.
Existing Instance poset_pord_subst.
Existing Instance poset_pord_partialorder.

Lemma poset_pord_subst_l (P: Poset)(x y z: P):
  x == y -> x <=p z -> y <=p z.
Proof.
  intros.
  assert (Hrefl: z == z) by reflexivity.
  now apply (poset_pord_subst H Hrefl).
Qed.  

Lemma poset_pord_subst_r (P: Poset)(x y z: P):
  y == z -> x <=p y -> x <=p z.
Proof.
  intros.
  assert (Hrefl: x == x) by reflexivity.
  now apply (poset_pord_subst Hrefl H).
Qed.  

Class Monotone (P Q: Poset) :=
  {
    monotone_map: Map P Q;
    monotone_preserve: Proper ((<=p) ==> (<=p)) monotone_map
  }.
Coercion monotone_map: Monotone >-> Map.
Existing Instance monotone_map.
Existing Instance monotone_preserve.

Instance Monotone_setoid (P Q: Poset): Setoid :=
  {
    carrier := Monotone P Q;
    equal f g := equal (Setoid := Map_setoid P Q) f g
  }.
Proof.
  split.
  - intros f x; reflexivity.
  - intros f g Heq x; symmetry; apply Heq.
  - intros f g h H H' x; transitivity (g x); [apply H | apply H'].
Defined.

Instance Monotone_comp {P Q R: Poset}(f: Monotone P Q)(g: Monotone Q R): Monotone P R :=
  {
      monotone_map := Map_comp f g
  }.
Proof.
  intros p q H; simpl.
  now do 2 apply monotone_preserve.
Defined.

Instance Monotone_id (P: Poset): Monotone P P :=
  {
    monotone_map := Map_id P
  }.
Proof.
  now intros p q H.
Defined.

Instance Posets: Category :=
  {
    obj := Poset;
    hom := Monotone_setoid;
    comp := @Monotone_comp;
    id := Monotone_id
  }.
Proof.
  - simpl; intros.
    rewrite (H x), (H0).
    reflexivity.
  - simpl; intros; reflexivity.
  - simpl; intros; reflexivity.
  - simpl; intros; reflexivity.
Defined.

Class KPL (C: Category)(T: C -> C)(K: Kleisli T)(pred: C -> Posets) :=
  {
    sbst: forall {X Y: C}, C X (T Y) -> Posets (pred Y) (pred X);

    sbst_subst: forall (X Y: C), Proper ((==) ==> (==)) (@sbst X Y);

    sbst_comp:
      forall (X Y Z: C)(f: hom X (T Y))(g: hom Y (T Z)),
        sbst f \o sbst g == sbst (bind g \o f);

    sbst_id:
      forall (X: C),
        id (pred X) == sbst (pure (X:=X))
  }.
Existing Instance sbst_subst.
Notation "f # P " := (sbst f P) (at level 45, right associativity).

Lemma hoare_id:
  forall `(kpl: @KPL C T K pr)(X: C)(P: pr X),
    P <=p pure#P.
Proof.
  intros.
  generalize (sbst_id (KPL:=kpl) (X:=X)); simpl; intro.
  apply (poset_pord_subst_r (H P)).
  reflexivity.
Qed.

Lemma hoare_comp:
  forall `(kpl: @KPL C T K pr)(X Y Z: C)(P: pr X)(Q: pr Y)(R: pr Z)
         (f: C X (T Y))(g: C Y (T Z)),
    P <=p f#Q ->
    Q <=p g#R ->
    P <=p (bind g \o f)#R.
Proof.
  intros.
  transitivity (f#Q); auto.
  transitivity (f # (g # R)).
  - apply monotone_preserve.
    assumption.
  - generalize (sbst_comp (KPL:=kpl) f g R); simpl; intro.
    apply (poset_pord_subst_r H1).
    reflexivity.
Qed.

Lemma hoare_trans_r:
  forall `(kpl: @KPL C T K pr)(X Y: C)(P: pr X)(Q R: pr Y)(f: C X (T Y)),
    P <=p f#Q -> Q <=p R -> P <=p f#R.
Proof.
  intros; apply transitivity with (f#Q); auto.
  rewrite H0.
  reflexivity.
Qed.
  
Instance function (X Y: Type): Setoid :=
  {
    carrier := X -> Y;
    equal f g := forall x, f x = g x
  }.
Proof.
  split.
  - intros f x; auto.
  - intros f g Heq x; auto.
  - intros f g h Heqfg Heqgh x.
    rewrite Heqfg; apply Heqgh.
Defined.

Instance Types: Category :=
  {
    obj := Type;
    hom X Y := function X Y;
    comp X Y Z f g x := g (f x);
    id X x := x
  }.
Proof.
  - simpl; intros.
    rewrite H, H0; auto.
  - simpl; intros; auto.
  - simpl; intros; auto.
  - simpl; intros; auto.
Defined.

Notation "m >>= f" := (bind (C:=Types) f m) (at level 53, left associativity).
Notation "x <- m ; p" := (m >>= fun x => p) (at level 60, right associativity).
Notation "x <-: m ; p" := (x <- pure m ; p ) (at level 60, right associativity).
Notation "f >> g" := (bind (C:=Types) g \o{Types} f) (at level 42, right associativity).

Instance Maybe: Kleisli (C:=Types) option :=
  {
    pure X x := Some x;
    bind X Y f m := match m with Some x => f x | _ => None end
  }.
Proof.
  - simpl; intros X [x|]; auto.
  - simpl; intros X Y f x; auto.
  - simpl; intros X Y Z f g [x|]; auto.
Defined.

Module Pred.
  Definition type (X: Type) := X -> Prop.
  Definition pord {X: Type}(P Q: type X) := forall x, P x -> Q x.
  Arguments pord {X}(P Q) /.
  Definition impl {X: Type}(P Q: type X) := fun x => P x -> Q x.
  Arguments impl {X}(P Q) x /.
  Definition not {X: Type}(P: type X) := fun x => ~ P x.
  Arguments not {X}(P) x /.
  Definition and {X: Type}(P Q: type X) := fun x => P x /\ Q x.
  Arguments and {X}(P Q) x /.
  Definition or {X: Type}(P Q: type X) := fun x => P x \/ Q x.
  Arguments or {X}(P Q) x /.
  Definition True := fun {X: Type}(_: X) => True.
  Definition False := fun {X: Type}(_: X) => False.
End Pred.
Notation predicate := Pred.type.

Instance Pred_setoid (X: Type): Setoid :=
  {
    carrier := predicate X;
    equal P Q := forall x, P x <-> Q x
  }.
Proof.
  split.
  - intros P x; tauto.
  - intros P Q H; symmetry; auto.
  - intros P Q R H H' x; transitivity (Q x); auto.
Defined.

Instance Pred_Poset (X: Type): Poset :=
  {
    poset_setoid := Pred_setoid X;
    poset_pord := Pred.pord
  }.
Proof.
  {
    intros P Q H P' Q' H' Hpp x; simpl in *.
    rewrite <- H', <- H; apply Hpp.
  }
  split; simpl.
  - now intros P; simpl; auto.
  - intros P Q R; simpl; intros Hpq Hqr x Hp.
    now apply Hqr, Hpq.
  - now intros P Q; simpl; intros Hpq Hqp x; split; revert x.
Defined.


Program Instance MaybeKPL: KPL Maybe Pred_Poset :=
  {
    sbst X Y f :=
      {| monotone_map :=
           {| map := fun P x => match f x with Some y => P y | _ => False end |} |}
  }.
Next Obligation.
  simpl; intros P Q H x.
  destruct (f x) as [y|]; auto.
  split; auto.
Qed.
Next Obligation.
  intros P Q; simpl; intros Hpq x.
  destruct (f x) as [y|]; [revert y |]; tauto.
Qed.
Next Obligation.
  intros f g H Q x; simpl.
  rewrite <- H.
  destruct (f x) as [y|]; tauto.
Qed.
Next Obligation.
  rename x into R, x0 into x.
  destruct (f x) as [y|]; tauto.
Qed.
Next Obligation.
  tauto.
Qed.

(* Notation "[ x <~ P ] ; m 'in' A ; [ y ~> Q ]" := (Pred.pord (fun x => P) (sbst (C:=Types)(KPL:=A) (fun x => m) (fun y => Q))) (at level 95). *)
(* Notation "[ x <~ P ] ; m ; [ y ~> Q ]" := ([ x <~ P ] ; m in _ ; [ y ~> Q ]) (at level 95). *)
Notation "'for' ( x : A ) 'with' P  ; 'result' y 'of' m 'in' KPL ; 'satisfies' Q" := (Pred.pord (fun (x:A) => P) (sbst (C:=Types)(KPL:=KPL) (fun x => m) (fun y => Q))) (at level 97, x at next level).
Notation "'for' ( x : A ) 'with' P  ; 'result' y 'of' m ; 'satisfies' Q" := (for (x : A) with P; result y of m in _; satisfies Q) (at level 97, x at next level).
Notation "'for' x 'with' P  ; 'result' y 'of' m 'in' KPL ; 'satisfies' Q" := (for (x : _) with P; result y of m in KPL; satisfies Q) (at level 97).
Notation "'for' x 'with' P  ; 'result' y 'of' m ; 'satisfies' Q" := (for x with P; result y of m in _; satisfies Q) (at level 97).

Lemma hcomp:
  forall {X Y Z: Type}(P: predicate X)(Q: predicate Y)(R: predicate Z)
         (f: X -> option Y)(g: Y -> option Z),
    (for x with P x; result y of f x in MaybeKPL; satisfies Q y) ->
    (for y with Q y; result z of g y in MaybeKPL; satisfies R z) ->
    (for x with P x; result z of y <- f x; g y in MaybeKPL; satisfies R z).
Proof.
  intros.
  apply (hoare_comp (kpl:=MaybeKPL)) with Q; assumption.
Qed.

Require Import Arith.
Fixpoint dif (n m: nat){struct m} :=
  match n, m with
  | S n', S m' => dif n' m'
  | _, 0 => Some n
  | 0, S _ => None
  end.

(* success *)
Goal
  forall n,
    for x with x = S n;
    result z of
           (y <-: (S x);
            dif y 2);
    satisfies z = n.
Proof.
  simpl; intros; subst.
  destruct n; ring.
Qed.


Lemma le_ind':
  forall (P : nat -> nat -> Prop),
    (forall n, P 0 n) ->
    (forall n m : nat, P n m -> P (S n) (S m)) ->
    forall n m : nat, le n m -> P n m.
Proof.
  intros.
  revert m H1; induction n.
  - intros; apply H.
  - destruct m.
    + intro H1; inversion H1.
    + intro Hle; apply H0, IHn, le_S_n; auto.
Qed.

Require Import Omega.
Goal
  for x with (2 <= x);
  result z of
         (mx <-: x * x;
          px <-: x + x;
          pure (px, mx));
  satisfies let (px,mx) := z in px <= mx.
Proof.
  simpl.
  intros.
  elim H; simpl; auto.
  intros.
  rewrite plus_comm; simpl.
  rewrite mult_comm; simpl.
  omega.
Qed.

Goal
  for nm with (let (n,m) := nm:nat*nat in n <= m);
  result z of (let (n,m) := nm:nat*nat in dif m n) in MaybeKPL;
  satisfies 0 <= z.
Proof.
  simpl; intros [n m] Hle; simpl in *.
  pattern n, m; apply le_ind'; auto; clear Hle n m.
  destruct n; simpl; auto with arith.
Qed.

(* main *)
Goal
    for x with 2 <= x;
    result z of
           (mx <-: x * x;
            px <-: x + x;
            dif mx px);
    satisfies 0 <= z.
Proof.
  change
    (for x with 2 <= x;
     result z of
            (mx <-: x * x;
             px <-: x + x;
             pm <-: (px,mx);     (* intermediate parameter *)
             let (p,m) := pm:_*_ in dif m p);
     satisfies 0 <= z).
  eapply (hoare_comp (kpl:=MaybeKPL)).
  - apply Unnamed_thm0.
  - apply Unnamed_thm1.
Qed.

(* failure *)
Goal
  forall P,
    ~ (for x with x = 0;
       result _ of y <-: (S x); dif y 2;
       satisfies P).
Proof.
  simpl; intros P H; generalize (H _ (eq_refl _)); simpl; auto.
Qed.

Require Import List.
Import List.ListNotations.

Definition head {X: Type}(l: list X): option X :=
  match l with
  | [] => None
  | x::_ => Some x
  end.

Definition tail {X: Type}(l: list X): option (list X) :=
  match l with
  | [] => None
  | _::ls => Some ls
  end.

Goal
  forall (X: Type),
    for (l: list X) with length l >= 1;
    result x of head l in MaybeKPL;
    satisfies exists y, x = y.
Proof.
  simpl; intros X [| x l]; simpl; auto.
  - intros H; inversion H.
  - intros; exists x; reflexivity.
Qed.

Goal
  forall {X: Type},
    ~ for (l: list X) with length l = 0;
    result _ of head l in MaybeKPL;
    satisfies True.
Proof.
  intros X H; simpl in *.
  generalize (H [] (eq_refl 0)); auto.
Qed.

Goal
  forall (X: Type)(x: X)(ls: list X),
    for (l: list X) with (l = x::ls);
    result p of (h <- head l;
                 t <- tail l;
                 pure (h,t)) in MaybeKPL;
    satisfies p = (x,ls).
Proof.
  simpl; intros X x ls [| z l]; simpl.
  - intros Heq; inversion Heq.
  - intros Heq; inversion Heq; subst; reflexivity.
Qed.

(* State Monad *)
Module PType.
  Inductive type := make { carrier: Type; point: carrier }.
End PType.
Notation PType := PType.type.
Coercion PType.carrier : PType >-> Sortclass.

Module SPred.
  Definition type (S: PType)(X: Type) := S -> X -> Prop.
  Definition pord {S: PType}{X: Type}(P Q: type S X) := forall s x, P s x -> Q s x.
  Arguments pord {S X}(P Q) /.
  Definition impl {S: PType}{X: Type}(P Q: type S X) := fun s x => P s x -> Q s x.
  Arguments impl {S X}(P Q) s x /.
  Definition not {S: PType}{X: Type}(P: type S X) := fun s x => ~ P s x.
  Arguments not {S X}(P) s x /.
  Definition and {S: PType}{X: Type}(P Q: type S X) := fun s x => P s x /\ Q s x.
  Arguments and {S X}(P Q) s x /.
  Definition or {S: PType}{X: Type}(P Q: type S X) := fun s x => P s x \/ Q s x.
  Arguments or {S X}(P Q) s x /.
  Definition True := fun {S: PType}{X: Type}(_: S)(_: X) => True.
  Definition False := fun {S: PType}{X: Type}(_: S)(_: X) => False.
End SPred.
Notation spredicate := SPred.type.

Instance SPred_setoid (S: PType)(X: Type): Setoid :=
  {
    carrier := spredicate S X;
    equal P Q := forall s x, P s x <-> Q s x
  }.
Proof.
  split.
  - intros P s x; tauto.
  - intros P Q H; symmetry; auto.
  - intros P Q R H H' s x; transitivity (Q s x); auto.
Defined.

Instance SPred_Poset (S: PType)(X: Type): Poset :=
  {
    poset_setoid := SPred_setoid S X;
    poset_pord := SPred.pord
  }.
Proof.
  {
    intros P Q H P' Q' H' Hpp s x; simpl in *.
    rewrite <- H', <- H; apply Hpp.
  }
  split; simpl.
  - now intros P; simpl; auto.
  - intros P Q R; simpl; intros Hpq Hqr s x Hp.
    now apply Hqr, Hpq.
  - now intros P Q; simpl; intros Hpq Hqp s x; split; revert s x.
Defined.

Definition state (S: PType)(X: Type) := S -> (X * S)%type.

Instance Setoids: Category :=
  {
    obj := Setoid;
    hom X Y := Map_setoid X Y;
    comp X Y Z f g := Map_comp f g;
    id X := Map_id X
  }.
Proof.
  - simpl; intros.
    rewrite H, H0; reflexivity.
  - simpl; intros; reflexivity.
  - simpl; intros; reflexivity.
  - simpl; intros; reflexivity.
Defined.

(* Instance State (S: PType): Kleisli (C:=Setoids) (state S) := *)
Axiom ext_eq: forall (A B: Type)(f g: A -> B),
    (forall x, f x = g x) -> f = g.
Instance State (S: PType): Kleisli (C:=Types) (state S) :=
  {
    pure X x := fun s => (x,s);
    bind X Y f m := fun s => let (y,s') := m s in f y s'
  }.
Proof.
  - simpl; intros X x.
    apply ext_eq; intros s.
    destruct (x s); reflexivity.
  - simpl; intros X Y f x; auto.
  - simpl; intros X Y Z f g x; auto.
    apply ext_eq; intros s.
    destruct (x s); reflexivity.
Defined.
Definition get {S: PType}: state S S := fun s => (s,s).
Definition put {S: PType}(s': S): state S unit := fun s => (tt,s').
Definition modify {S: PType}(f: PType.carrier S -> PType.carrier S): state S unit
  := s <- get; put (f s).


Program Instance StateKPLMap (S: PType){X Y: Type}(f: X -> state S Y)
  : Map (SPred_setoid S Y) (SPred_setoid S X) :=
  { map := fun P s x => let (y,s') := f x s in P s' y }.
Next Obligation.
  intros P Q Heq s x.
  destruct (f x s); apply Heq.
Qed.

Program Instance StateKPL (S: PType): KPL (State S) (SPred_Poset S) :=
  {
    sbst X Y f :=
      {| monotone_map := StateKPLMap S f |}
  }.
Next Obligation.
  intros P Q; simpl; intros Hpq s x.
  destruct (f x s); apply Hpq.
Qed.
Next Obligation.
  intros f g H Q s x; simpl.
  rewrite <- H.
  destruct (f x s); reflexivity.
Qed.
Next Obligation.
  rename x into R, x0 into x.
  destruct (f x s); reflexivity.
Qed.
Next Obligation.
  tauto.
Qed.

Notation "'from' s 'in' S ; 'for' ( x : A ) 'with' P  ; 'result' y 'of' m ; 'into' t ; 'satisfies' Q" := (SPred.pord (fun (s:S)(x:A) => P) (sbst (C:=Types)(KPL:=StateKPL _) (fun x => m) (fun (t: S) y => Q))) (at level 97, x at next level).
Notation "'from' s 'in' S ; 'for' x 'with' P  ; 'result' y 'of' m ; 'into' t ; 'satisfies' Q" := (from s in S; for (x:_) with P; result y of m; into t; satisfies Q) (at level 97).

Definition Pnat := PType.make 0.
Goal
  from s in Pnat;
  for x with (2 <= x);
  result z of
         (mx <-: x * x;
          px <-: x + x;
          pure (mx, px));
  into s';
  satisfies (let (mx,px) := z in px <= mx).
Proof.
  intros s x H; simpl.
  elim H; simpl; auto.
  intros.
  rewrite plus_comm, mult_comm; simpl.
  omega.
Qed.

Goal
  from s in Pnat;
  for (x: nat) with (1 <= s);
  result z of pure x;
  into s';
  satisfies (1 <= s').
Proof.
  intros s x H; simpl; auto.
Qed.

(* カウント付き比較 *)
Fixpoint leb_c (n m: nat): state Pnat bool :=
  match n, m with
  | O, O | O, S _ => _ <- modify (S:=Pnat) S
                     ; pure true
  | S _, O => _ <- modify (S:=Pnat) S
              ; pure false
  | S p, S q => leb_c p q
  end.
Functional Scheme leb_c_ind := Induction for leb_c Sort Prop.

(* 比較すれば比較回数は真に大きくなるよ *)
Fixpoint insert (n: nat)(l: list nat): state Pnat (list nat) :=
  match l with
  | nil => pure (cons n nil)
  | cons m xs => b <- leb_c n m
                 ; (if b: bool
                    then pure (cons n l)
                    else (res <- insert n xs
                          ; pure (cons m res)))
  end.

Fixpoint insertion_sort (l: list nat): state Pnat (list nat) :=
  match l with
  | nil => pure nil
  | cons n xs => res <- insertion_sort xs
                 ; insert n res
  end.

(* 大雑把な評価 *)
Goal
  forall c,
    from s in Pnat;                 (* 状態 s から始めて *)
    for (l: list nat) with (s = c); (* 値 l と条件 s = c について *)
    result l' of insertion_sort l;  (* insertion_sort l を計算した結果 l' が *)
    into s';                        (* 状態 s' に至ったとすると *)
    satisfies (s' <= c + length l' * length l'). (* これらは s' <= c + length l' * length l' を満たす *)
Admitted.

Goal
  from s in Pnat;
  for (l: list nat) with (s = 0);
  result l' of insertion_sort l;
  into s';
  satisfies (s' <= length l' * length l').
Proof.
  apply Unnamed_thm9.
Qed.

(* 一筋縄じゃいかねぇ *)