Search code examples
haskellcoq

Coq extraction to Haskell

I have the following Coq implementation of integer division with remainder. When I extract it to Haskell everything works fine. I compared the Coq version to the generated Haskell version and tried to understand what's going on. It seems that rewrite is simply removed here, and what actually steers the extraction here are induction, destruct, exists and specialize. Is there any scenario where rewrite is used during extraction? Also, some variables names are kept (like q0 and m0'') but others change (r0 to h) is there any reason to change names? Here is the Coq code followed by the extracted code:

(***********)
(* IMPORTS *)
(***********)
Require Import Coq.Arith.PeanoNat.
Require Import Coq.Structures.OrdersFacts.

Lemma Sn_eq_Sm: forall n m,
  (n = m) -> ((S n) = (S m)).
Proof.
  intros n m H.
  rewrite H.
  reflexivity.
Qed.

Lemma Sn_lt_Sm: forall n m,
  (n < m) -> ((S n) < (S m)).
Proof.
  intros n0 m0 H.
  unfold lt in H.
  apply Nat.lt_succ_r.
  apply H.
Qed.

Lemma add_nSm : forall (n m : nat),
  (n + (S m)) = S (n + m).
Proof.
  intros n m.
  induction n.
  - reflexivity.
  - simpl.
    apply Sn_eq_Sm.
    apply IHn.
Qed.

Lemma n_lt_m: forall n m,
  ((n <? m) = false) -> (m <= n).
Proof.
Admitted.

Lemma n_le_m_le_n: forall n m,
  (n <= m) -> ((m <= n) -> (m = n)).
Proof.
Admitted.

Lemma Sn_ge_0: forall n,
  0 <= (S n).
Proof.
  induction n as [|n' IHn'].
  - apply le_S. apply le_n.
  - apply le_S. apply IHn'.
Qed.

Lemma n_ge_0: forall n,
  0 <= n.
Proof.
  induction n as [|n' IHn'].
  - apply le_n.
  - apply le_S. apply IHn'.
Qed.

Lemma Sn_gt_0: forall n,
  0 < (S n).
Proof.
  induction n as [|n' IHn'].
  - apply le_n.
  - apply le_S. apply IHn'.
Qed.

Lemma n_le_m_implies_Sn_le_Sm: forall n m,
  (n <= m) -> ((S n) <= (S m)).
Proof.
  induction n as [|n' IHn'].
  - induction m as [|m' IHm'].
    + intros H1. apply le_n.
    + intros H1. apply le_S.
      apply IHm'. apply n_ge_0.
  - induction m as [|m' IHm'].
    + intros H1. inversion H1. 
    + intros H1. inversion H1. 
      apply le_n. apply IHm' in H0 as H2.
      apply le_S in H2. apply H2.
Qed.

(****************************************)
(* division with quotient and remainder *)
(****************************************)
Definition div_q_r: forall n m : nat,
   {     q:nat & {     r:nat | (n = q * (S m) + r) /\ (r < (S m))}}.
Proof.
  induction n as [|n' IHn'].
  - exists 0. exists 0. split. reflexivity. apply Sn_gt_0.
  - intros m0.
    destruct m0 as [|m0''] eqn:E1.
    + exists (S n'). exists 0. split.
      * rewrite Nat.add_0_r with (n:=(S n') * 1).
        rewrite Nat.mul_1_r with (n:=(S n')). reflexivity.
      * specialize Sn_gt_0 with (n:=0). intros H. apply H.
    + specialize IHn' with (m:=(S m0'')).
      destruct IHn' as [q0 H]. destruct H as [r0 H].
      destruct (r0 <? (S m0'')) eqn:E2.
      * exists q0. exists (S r0). split.
        -- rewrite add_nSm with (n:=q0 * S (S m0'')). 
           apply Sn_eq_Sm. apply proj1 in H as H1. apply H1.
        -- apply Nat.ltb_lt in E2. apply Sn_lt_Sm. apply E2.
      * exists (S q0). exists 0. split.
        -- apply proj2 in H as H2. rewrite Nat.lt_succ_r in H2.
           apply n_lt_m in E2. apply n_le_m_le_n in H2.
           apply proj1 in H as H1. rewrite H2 in H1. rewrite H1.
           rewrite <- add_nSm with (n:=q0 * S (S m0'')) (m:=S m0'').
           rewrite Nat.add_0_r.
           rewrite Nat.mul_succ_l with (n:=q0) (m:=S (S m0'')).
           reflexivity. apply E2.
        -- unfold "<". apply n_le_m_implies_Sn_le_Sm. apply Sn_ge_0.
Qed.

(********************************)
(* Extraction Language: Haskell *)
(********************************)
Extraction Language Haskell.

(***************************)
(* Use Haskell basic types *)
(***************************)
Require Import ExtrHaskellBasic.

(****************************************)
(* Use Haskell support for Nat handling *)
(****************************************)
Require Import ExtrHaskellNatNum.
Extract Inductive Datatypes.nat => "Prelude.Integer" ["0" "Prelude.succ"]
"(\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))".

(***************************)
(* Extract to Haskell file *)
(***************************)
Extraction "/home/oren/GIT/some_file_Haskell.hs" div_q_r.

And here is the extracted Haskell code:

div_q_r :: Prelude.Integer -> Prelude.Integer -> SigT Prelude.Integer
           Prelude.Integer
div_q_r n =
  nat_rec (\_ -> ExistT 0 0) (\n' iHn' m0 ->
    (\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))
      (\_ -> ExistT (Prelude.succ n')
      0)
      (\m0'' ->
      let {iHn'0 = iHn' (Prelude.succ m0'')} in
      case iHn'0 of {
       ExistT q0 h ->
        let {b = ltb h (Prelude.succ m0'')} in
        case b of {
         Prelude.True -> ExistT q0 (Prelude.succ h);
         Prelude.False -> ExistT (Prelude.succ q0) 0}})
      m0) n
Solution

  • When you use rewrite, the goal is actually a type (a formula) and the type of this type is often Prop. When this happens, as in your example, the effect of the rewrite tactic is discarded because the part of the term where it took place was discarded.

    the extraction tool does not look at tactics: it remove expressions whose type has type Prop from the term that will be executed. The whole system is designed in such a way that these expressions should not have an effect on computation.

    In a sense, it is a distinction between compile-time verification and run-time verification. All the proofs that you do in Coq are compile-time verifications, at run-time they don't need to be redone, so they are removed from the code. The Prop sort is used to mark computations that happen only at compile-time and won't have an effect on the execution at run-time.

    You can somehow predict the content of the Haskell extracted program by looking at the result of Print div_q_r.

    The result contains instances of existT and instance of exist. The type of existT is :

    forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x}

    The notation {x : A & P x} is for @sigT A P. In turn the type of sigT is

    forall A : Type, (A -> Type) -> Type

    The type of existT P xx pp is @sigT A P and the type of the latter is Type. In consequence, the extraction tool decides that this term contains data that is important at run time. Moreover, the second component of sigT A P, has type P xx which itself has type Type, so this also is important at run time: it won't be discarded.

    Now let's turn our attention to expression of the form exist _ _. Such an expression has type @sig A P and sig has type :

    forall A: Type, (A -> Prop) -> Type

    So an expression exist Q y qq contains y whose type has type Type and qq whose type is Q y and has type Prop. Information on how to compute y will be kept at run time, but information on how to compute qq is discarded.

    If you want to know where rewrite had an effect in the proof, you only need to look for instances of eq_ind and eq_ind_r in the result of Print div_q_r. You will see that these instances are subterms of the third argument of exist statements. This is the reason why they don't appear in the final result. It is not because the extraction has special treatement of rewrites, it is because it has a special behavior on the type of types Prop (we also call it the sort Prop).

    It is possible to construct functions where rewrite leaves a trace in the extraction result, but I am not sure that these functions behave correctly in Haskell. This when, the formula where the rewrite occur is not in sort Prop.

    Definition nat_type n :=
  match n with O => nat | S p => bool end.

Definition strange n : nat_type (n * 0).
rewrite Nat.mul_0_r.
exact n.
Defined.