The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Does anyone have experience debugging Extraction Inline failures with 
Unset Extraction SafeImplicits?  I just tried this for the first time, 
and am not understanding what went wrong based on the comment placed in 
the output by Unset Extraction SafeImplicits. The warning is:

Warning:
 At least an implicit occurs after extraction : 3rd argument (a) of wfi_lt.
 Extraction SafeImplicits is unset, extracting nonetheless,
 but this code is potentially unsafe, please review it manually.

The Coq script is attached.  The key extracted function is:

  let merge_sort d ls =
    let rec f _ =
      let iH = fun y -> f y in
      (fun d0 ls0 _ ->
      let (ls1, ls2) = split ls0 in
      (match ls2 with
       | [] -> ls1
       | _ :: _ -> merge_acc d0 (iH (length ls1) (not d0) ls1 __) (iH 
(length ls2) (not d0) ls2 __) []))
    in f __ (* 3rd argument (a) of wfi_lt *) d ls __
 end

It looks to me like the first arg of f is understood as not used by 
extraction.   So, what is the comment saying about that arg?

The function wfi_lt (well-founded induction using lt) was defined with:


Definition wfi_lt := well_founded_induction_type Wf_nat.lt_wf.

Extraction Implicit wfi_lt [1 3].

Extraction Inline wfi_lt.


Interestingly, merge_acc also uses wfi_lt, but extraction had no 
difficulty with it:


  let rec merge_acc d ls1 ls2 acc =
    match ls1 with
    | [] ->
      (match ls2 with
       | [] -> acc
       | b :: ls4 -> merge_acc d [] ls4 (b :: acc))
    | a :: ls3 ->
      (match ls2 with
       | [] -> merge_acc d [] ls3 (a :: acc)
       | b :: ls4 -> if le_or_ge_dec d a b then merge_acc d ls1 ls4 (b 
:: acc) else merge_acc d ls3 ls2 (a :: acc))


This is using 8.5pl1

Thanks,

-- Jonathan


Require Import Coq.Lists.List.
Import ListNotations.
Require Import Omega.
Require Import Coq.Classes.RelationClasses.

Ltac revert_all :=
  repeat lazymatch goal with H :_ |- _ => revert H end.

Ltac intro_to hyp :=
  intro;
  lazymatch goal with
  | H :_ |- _ => tryif constr_eq H hyp then idtac else intro_to hyp
  end.

Definition wfi_lt := well_founded_induction_type Wf_nat.lt_wf.

Tactic Notation "wfinduction" constr(term) "as" ident(H) :=
  let R := fresh in
  let E := fresh in
  remember term as R eqn:E;
  move R at top; revert E; revert_all;
  induction R as [R H] using wfi_lt;
  intro_to E; subst R.

Ltac wfisolve := rewrite ?app_length in *; cbn in *; omega.

Lemma app_cons_rw : forall {T} ls1 (a : T) ls2, ls1 ++ a :: ls2 = (ls1 ++ [a]) ++ ls2.
Proof.
  intros. rewrite <-app_assoc. cbn. reflexivity.
Qed.

(*A fully-dependently-typed merge sort, starting from scratch.*)
Module MergeSort.
  Parameter A : Type.
  Parameter eq_dec : forall (a b : A), {a = b} + {a <> b}.
  Parameter le : A -> A -> Prop.
  Parameter le_ge_dec : forall (a b : A), {le a b} + {le b a}.
  Context (le_pre : PreOrder le).
  Context (le_po : PartialOrder eq le).

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

  Fixpoint count (x : A)(ls : list A) : nat :=
    match ls with
    | [] => 0
    | a :: ls' => (if (a =! x) then 1 else 0) + count x ls'
    end.

  Lemma count_app : forall x ls1 ls2, count x (ls1 ++ ls2) = count x ls1 + count x ls2.
  Proof.
    induction ls1. all:cbn. all:intros. 1:reflexivity.
    specialize (IHls1 ls2). omega.
  Qed.

  Lemma count_length : forall x ls, count x ls <= length ls.
  Proof.
    induction ls as [|a ls]. all:cbn. 1:omega. 
    destruct (a =! x). all:omega.
  Qed.

  Notation mem x ls := (count x ls > 0).

  Definition permut ls1 ls2 := (forall x, count x ls1 = count x ls2).

  Lemma permut_transitive : Transitive permut.
  Proof.
    intros ls1 ls2 ls3 H1 H2.
    unfold permut in *.
    intro x.
    specialize (H1 x).
    specialize (H2 x).
    congruence.
  Qed.

  Instance permut_equivalence : Equivalence permut.
  Proof.
    split. 3:apply permut_transitive.
    all:simpl_relation.
  Qed.

  (*Not a fully specified remove function, but sufficient for its use here:*)
  Local Definition remove1 a ls :
    mem a ls -> { rls | length ls = S (length rls) /\ permut ls (a::rls) }.
  Proof.
    induction ls as [|b ls IHls]. all:cbn. all:intro H. 1:omega.
    case (a =! b); intros.
    - subst b. exists ls. split. all:reflexivity.
    - edestruct IHls as [rls (H1 & H2)].
      { destruct (b =! a). 1:congruence. omega. }
      exists (b::rls). unfold permut in *. cbn. split. 1:omega.
      intro x. destruct (a =! x).
      + subst x. destruct (b =! a). 1:congruence.
        pose proof (H2 a). cbn in *. destruct (a =! a). 1:omega. congruence.
      + pose proof (H2 x). cbn in *. destruct (a =! x). 1:congruence. omega.
  Qed.

  Lemma permut_length ls1 ls2 : permut ls1 ls2 -> length ls1 = length ls2.
  Proof.
    unfold permut.
    wfinduction (length (ls1++ls2)) as IH.
    destruct ls1 as [|a ls1]. all:cbn. all:intro H.
    - destruct ls2 as [|b ls2]. 1:reflexivity.
      specialize (H b). cbn in H. destruct (b =! b). 1:omega. congruence.
    - pose proof (H a) as Ha. destruct (a =! a) as [_|?]. 2:congruence.
      edestruct (remove1 a ls2) as (ls2a & H1 & H2). 1:omega.
      rewrite H1. f_equal.
      unshelve eapply (IH _ _ ls1 ls2a eq_refl). 1:wfisolve.
      intro x. pose proof (H x) as Hx. pose proof (H2 x) as Hx2.
      all:cbn in *. destruct (a =! x). all:subst. all:omega.
  Qed.

  Lemma permut_app : forall ls1 ls2 ls3 ls4, permut ls1 ls3 -> permut ls2 ls4 -> permut (ls1 ++ ls2) (ls3 ++ ls4).
  Proof.
    intros ls1 ls2 ls3 ls4 H1 H2.
    intro x. specialize (H1 x). specialize (H2 x).
    rewrite ?count_app. omega.
  Qed.

  Definition le_or_ge (direction : bool)(a b : A) := if direction then le a b else le b a.

  Notation "a <=[ d ]>= b" := (le_or_ge d a b) (at level 70, no associativity,
                                               format "a  <=[ d ]>=  b").

  Definition le_or_ge_dec d a b : {a<=[d]>=b}+{b<=[d]>=a}.
  Proof.
    destruct d. all:cbn.
    - apply le_ge_dec.
    - apply le_ge_dec.
  Qed.

  Lemma le_or_ge_transitive : forall d, Transitive (le_or_ge d).
  Proof.
    intros (). all:cbv. all:intros x y z H1 H2. all:etransitivity. all:eassumption.
  Qed.

  Instance le_or_ge_preorder d : PreOrder (le_or_ge d).
  Proof.
    split. 2:apply le_or_ge_transitive. destruct d. all:simpl_relation.
  Qed.

  Instance le_or_ge_partial_order d : PartialOrder eq (le_or_ge d).
  Proof.
    pose proof (partial_order_antisym le_po) as POA.
    destruct d. all:cbv. all:intros a b.
    all:destruct (eq_dec a b). all:simpl_relation.
  Qed.

  (*directional sorting:*)
  Definition dsorted d (ls : list A) := forall ls1 x ls2 y ls3, ls = ls1 ++ x::ls2 ++ y::ls3 -> x<=[d]>=y.

  Lemma dsorted_le d : forall ls1 x ls2 y ls3, dsorted d (ls1 ++ x::ls2 ++ y::ls3) -> x<=[d]>=y.
  Proof.
    intros * H. eapply H. reflexivity.
  Qed.

  Lemma dsorted_nil d : dsorted d [].
  Proof.
    intros ? * ?%app_cons_not_nil. contradiction.
  Qed.

  Lemma dsorted_single d : forall n, dsorted d [n].
  Proof.
    intros ? () * [= -> ?%app_cons_not_nil]. all:contradiction.
  Qed.

  Lemma dsorted_tail d : forall a ls, dsorted d (a :: ls) -> dsorted d ls.
  Proof.
    intros * H. unfold dsorted. intros * ->. apply (H (_::_) _ _ _ _ eq_refl).
  Qed.

  Lemma dsorted_head d : forall a b ls, dsorted d (a::b::ls) -> a<=[d]>=b.
  Proof.
    intros * H. apply (H [] _ [] _ _ eq_refl).
  Qed.

  Lemma dsorted_cons d : forall a b ls, dsorted d (b::ls) -> a<=[d]>=b -> dsorted d (a::b::ls).
  Proof.
    intros * H1 H2. unfold dsorted. intros () ? ls2 ? ? [= -> H].
    - revert H. destruct ls2. all:intros [= -> ->]. 1:assumption.
      etransitivity. 1:eassumption. apply (H1 [] _ _ _ _ eq_refl).
    - rewrite H in H1. apply (H1 _ _ _ _ _ eq_refl).
  Qed.

  Hint Rewrite @app_comm_cons @app_assoc : assoc_rws.

  Lemma dsorted_app d : forall ls1 ls2, dsorted d (ls1 ++ ls2) -> dsorted d ls1 /\ dsorted d ls2.
  Proof.
    intros * H. split. all:intros ? * -> .
    1:eapply (H _ _ _ _ (_ ++ _)). 2:eapply (H (_ ++ _) _ _ _ _).
    all:autorewrite with assoc_rws. all:reflexivity.
  Qed.

  Lemma dsorted_splice d : forall ls1 a ls2 b ls3,
      dsorted d (ls1 ++ a::ls2) -> dsorted d (ls2 ++ b::ls3) -> a<=[d]>=b -> dsorted d (ls1 ++ a::ls2 ++ b::ls3).
  Proof.
    induction ls1.
    - intros ? () **. all:cbn in *.
      + apply dsorted_cons. all:assumption.
      + apply dsorted_cons. 1:assumption.
        eapply dsorted_head. eassumption.
    - intros. destruct ls1. all:cbn in *.
      + apply dsorted_cons.
        * apply IHls1. 1:eapply dsorted_tail. all:eassumption.
        * eapply dsorted_head. eassumption.
      + apply dsorted_cons.
        * apply IHls1. 1:eapply dsorted_tail. all:eassumption.
        * eapply dsorted_head. eassumption.
  Qed.

  Lemma dsorted_flip d : forall ls, dsorted d ls <-> dsorted (negb d) (rev ls).
  Proof.
    induction ls. all:cbn [rev]. all:split. all:intro H.
    - apply dsorted_nil.
    - apply dsorted_nil.
    - destruct ls. 1:apply dsorted_single.
      apply dsorted_head in H as H1.
      apply dsorted_tail in H as H2.
      apply dsorted_tail in H2 as H3.
      cbn [rev]. rewrite <-app_assoc. eapply dsorted_splice.
      + apply IHls. assumption.
      + apply dsorted_single.
      + destruct d. all:assumption.
    - destruct ls. 1:apply dsorted_single.
      cbn [rev] in H.
      destruct (dsorted_app _ _ _ H) as [H1 _].
      rewrite <-app_assoc in H.
      apply dsorted_le in H as H2.
      apply <-IHls in H1.
      apply dsorted_cons. 2:destruct d. all:assumption.
  Qed.

  Definition split_acc (ls : list A) : forall acc1 acc2,
      (length acc1 = length acc2 \/ length acc1 = S (length acc2)) ->
      { lss | (length (fst lss) = length (snd lss) \/ length (fst lss) = S (length (snd lss)))
              /\ permut (ls ++ acc1 ++ acc2) (fst lss ++ snd lss) }.
  Proof.
    induction ls as [|a ls IHls]. all:intros acc1 acc2 H.
    { exists (acc1, acc2). cbn. split. 1:assumption. reflexivity. }
    destruct (IHls (a::acc2) acc1) as [[ls1 ls2] (H1 & H2)].
    { cbn. omega. }
    cbn [fst snd] in *.
    exists (ls1, ls2). cbn. split. 1:assumption.
    intro x. specialize (H2 x).
    autorewrite with assoc_rws in *. rewrite ?count_app in *. cbn in *. omega.
  Qed.

  Definition split (ls : list A) :
    { lss | (length (fst lss) = length (snd lss) \/ length (fst lss) = S (length (snd lss)))
            /\ permut ls (fst lss ++ snd lss) }.
  Proof.
    destruct (split_acc ls [] []) as [lss (H1 & H2)]. 1:omega.
    exists lss. split. 1:omega.
    intro x. specialize (H2 x). rewrite ?count_app in *. cbn in *. omega.
  Qed.

  Definition merge_acc d (ls1 ls2 acc : list A) :
    { ls | (dsorted (negb d) ((rev acc) ++ ls1) -> dsorted (negb d) ((rev acc) ++ ls2) -> dsorted d ls)
           /\ permut ls (ls1 ++ ls2 ++ acc) }.
  Proof.
    wfinduction (length (ls1 ++ ls2)) as IH.
    destruct (ls1) as [|a ls3] eqn:Els1, (ls2) as [|b ls4] eqn:Els2.
    - exists acc. cbn. rewrite app_nil_r. split. 2:reflexivity.
      intros. rewrite dsorted_flip. assumption.
    - unshelve eelim (IH _ _ d [] ls4 (b::acc) eq_refl). 1:wfisolve.
      intros ls (H1 & H2).
      exists ls. cbn -[count] in *. split.
      + intros H3 H4. rewrite app_nil_r in *.
        rewrite app_cons_rw in H4. destruct (dsorted_app _ _ _ H4) as (H5 & _).
        apply H1. all:assumption.
      + intro x. specialize (H2 x). rewrite app_comm_cons. rewrite count_app in *. cbn [count] in *. omega.
    - unshelve eelim (IH _ _ d [] ls3 (a::acc) eq_refl). 1:wfisolve.
      intros ls (H1 & H2).
      exists ls. cbn -[count] in *. split.
      + intros H3 H4. rewrite app_nil_r in *.
        rewrite app_cons_rw in H3. destruct (dsorted_app _ _ _ H3) as (H5 & _).
        apply H1. all:assumption.
      + intro x. specialize (H2 x). rewrite app_comm_cons. rewrite count_app in *. cbn [count] in *. omega.
    - case (le_or_ge_dec d a b). all:intro C.
      + unshelve eelim (IH _ _ d ls1 ls4 (b::acc) eq_refl). all:subst. 1:wfisolve.
        intros ls (H1 & H2).
        exists ls. cbn -[count] in *. split.
        * intros H3 H4. apply H1.
          -- rewrite <-app_assoc. eapply dsorted_splice.
             ++ rewrite app_cons_rw in H4. apply dsorted_app in H4. tauto.
             ++ apply dsorted_app in H3. tauto.
             ++ destruct d. all:assumption.
          -- rewrite <-app_assoc. cbn. assumption.
        * intro x. specialize (H2 x). autorewrite with assoc_rws in *. rewrite ?count_app in *.
          cbn [count] in *. omega.
      + unshelve eelim (IH _ _ d ls3 ls2 (a::acc) eq_refl). all:subst. 1:wfisolve.
        intros ls (H1 & H2).
        exists ls. cbn -[count] in *. split.
        * intros H3 H4. apply H1.
          -- rewrite <-app_assoc. cbn. assumption.
          -- rewrite <-app_assoc.  eapply dsorted_splice.
             ++ rewrite app_cons_rw in H3. apply dsorted_app in H3. tauto.
             ++ apply dsorted_app in H4. tauto.
             ++ destruct d. all:assumption.
        * intro x. specialize (H2 x). autorewrite with assoc_rws in *. rewrite ?count_app in *.
          cbn [count] in *. omega.
  Qed.

  Definition merge_sort d ls : { rls | dsorted d rls /\ permut ls rls }.
  Proof.
    wfinduction (length ls) as IH.
    case (split ls).
    intros (ls1 & ls2) (H1 & H2).
    cbn [fst snd] in *.
    destruct (ls2) as [|a ls3] eqn:els2.
    - exists ls1. cbn in *. destruct H1.
      + apply length_zero_iff_nil in H. subst. split.
        * apply dsorted_nil.
        * intro x. specialize (H2 x). cbn in *. assumption.
      + destruct ls1 as [|a ls1].
        * cbn in H. discriminate.
        * cbn in *. injection H. clear H. intro H. apply length_zero_iff_nil in H. subst. split.
          -- apply dsorted_single.
          -- intro x. specialize (H2 x). cbn in *. assumption.
    - apply permut_length in H2 as H2'.
      unshelve eelim (IH _ _ (negb d) ls1 eq_refl). 1:wfisolve.
      intros rls1 (H3 & H4).
      unshelve eelim (IH _ _ (negb d) ls2 eq_refl). all:subst. 1:wfisolve.
      intros rls2 (H5 & H6).
      elim (merge_acc d rls1 rls2 []).
      intros rls (H7 & H8).
      cbn [rev app] in H7. rewrite ?app_nil_r in H8.
      exists rls. split.
      + apply H7. all:assumption.
      + etransitivity. 1:eassumption.
        etransitivity. 2:symmetry. 1:apply permut_app. all:eassumption.
  Qed.

End MergeSort.
Import MergeSort.

Require Import ExtrOcamlNatInt.
Extraction Inline le_ge_dec.
Extract Inlined Constant eq_dec => "(=)".
Extract Inlined Constant le_ge_dec => "(<=)".
Extract Inlined Constant length => "length".
Extract Inlined Constant negb => "not".
Extract Inlined Constant app => "append".
Print wfi_lt.
Extraction Implicit wfi_lt [1 3].
Extraction Inline wfi_lt.
Unset Extraction SafeImplicits.
Recursive Extraction MergeSort.