Добыча Coq в Haskell

Question

У меня есть следующая реализация Coq целочисленного деления с остатком. Когда я распаковываю его на Haskell , все отлично работает . Я сравнил версию Coq с созданной версией Haskell и попытался понять, что происходит. Кажется, что rewrite просто удалено здесь , и что фактически управляет извлечением здесь: induction, destruct, exists и specialize. Есть ли сценарий, где rewrite используется во время извлечения? Кроме того, некоторые имена переменных сохраняются (например, q0 и m0''), но другие изменяются (r0 на h). Есть ли причина для изменения имен? Вот код Coq, за которым следует извлеченный код:

(***********)
(* 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.

А вот извлеченный код на Haskell:

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

Answer 1

Каждый раз, когда вы используете rewrite, целью является тип (формула), чей собственный тип - Prop.Таким образом, эффект тактической воли rewrite отбрасывается, потому что часть термина, в которой он имел место, была отброшена.

инструмент извлечения не смотрит на тактику: он удаляет выражения, тип которых имеет тип Propот срока, который будет выполнен.Вся система спроектирована таким образом, что эти выражения не должны влиять на вычисления.

В некотором смысле, это различие между проверкой во время компиляции и проверкой во время выполнения.Все доказательства, которые вы делаете в Coq, - это проверки во время компиляции, во время выполнения их не нужно переделывать, поэтому они удаляются из кода.Сортировка Prop используется для пометки вычислений, которые происходят только во время компиляции и не влияют на выполнение во время выполнения.

Вы можете каким-то образом предсказать содержимое извлеченной программы на Haskell с помощьюглядя на результат Print div_q_r.

Результат содержит экземпляры existT и экземпляр exist.Тип existT:

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

Обозначение {x : A & P x} для @sigT A P.В свою очередь тип sigT равен

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

Тип existT P xx pp равен @sigT A P, а тип последнего - Type.В результате инструмент извлечения решает, что этот термин содержит данные, которые важны во время выполнения.Более того, второй компонент sigT A P имеет тип P xx, который сам имеет тип Type, так что это также важно во время выполнения: он не будет отброшен.

Теперь давайте обратим наше вниманиедо выражения вида exist _ _.Такое выражение имеет тип @sig A P и sig имеет тип:

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

Таким образом, выражение exist Q y qq содержит y, тип которого имеет тип Type и qq, тип которого Q y и имеет тип Prop.Информация о том, как вычислять y, будет храниться во время выполнения, но информация о том, как вычислять qq, отбрасывается.

Если вы хотите знать, где rewrite оказал влияние в доказательстве, выНужно только искать экземпляры eq_ind и eq_ind_r в результате Print div_q_r.. Вы увидите, что эти экземпляры являются подтермами третьего аргумента операторов exist.Это причина, почему они не появляются в конечном результате.Это не потому, что извлечение имеет специальную обработку перезаписей, а потому, что оно имеет специальное поведение для типов типов Prop (мы также называем это sort Prop).

Можно построить функции, в которых rewrite оставляет след в результате извлечения, но я не уверен, что эти функции работают в Haskell правильно.

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.