The Coq mailing list

[Pierre Letouzey <pierre.letouzey AT inria.fr>]

----- Mail original -----
> 
> This leads me to the second part of your report, which is far more severe:
> something informative (in Coq's type "sum") is suddenly considered as
> logical by the system (i.e. acceptable in sort "Prop"), and hence discarded
> by the extraction, leading to this faulty "match __ with ...". This is
> normally impossible in the good old theory of Coq, but this theory around
> universes has been so much tweaked in the recent years (Hugo) and months
> (Matthieu) that the very foundational principles of extraction need to be
> re-asserted, and probably adapted, as shown by this bug. Once again, I'll
> let you know when I know more.
> 
> Best regards,
> Pierre Letouzey
> 

Hi again

The "sum" instance being in "Prop" was actually a bug, now fixed in coq trunk
by Matthieu (commit 2b833c49). Since this commit, your development needs to be
slightly adapted accordingly :
 - in Prefix.prefix_common you cannot inverse an "exists" to build
   a "sum", now that this "sum" isn't in Prop anymore. 
 - in Combi, a few "H" are now "X"
 - in DeflateCoding, a few "sum" should rather be some "or" now.
Here comes a temptative patch. With it, things compile and extract nicely
(even if I've still the issue with Vector.t/VectorDef.t to investigate).

Best regards
Pierre
diff --git a/Combi.v b/Combi.v
index ecacabc..0d7c5c3 100644
--- a/Combi.v
+++ b/Combi.v
@@ -1134,7 +1134,7 @@ Proof.
   assert (dc: {n | ~ Q (Vnth e n)} + ({n | ~ Q (Vnth e n)} -> False)).
   apply (dec_in_dec _ (fun n => ~ Q n)).
   intros a.
-  elim (H a).
+  elim (X a).
   intros Qa.
   apply inr. auto.
   intros nQa.
@@ -1151,7 +1151,7 @@ Proof.
   apply inl.
   apply forall_notexists.
   intros a.
-  apply H.
+  apply X.
   apply nex.
 Defined.
 
diff --git a/DeflateCoding.v b/DeflateCoding.v
index 1ce5902..c76921a 100644
--- a/DeflateCoding.v
+++ b/DeflateCoding.v
@@ -1019,7 +1019,7 @@ Proof.
   apply b1_lt_a1.
 Defined.
 
-Lemma sorting_rmdup : forall n L, Sorted (fun x y => ((x = y) + (mys (n:=n) x y))%type) L ->
+Lemma sorting_rmdup : forall n L, Sorted (fun x y => ((x = y) \/ (mys (n:=n) x y))%type) L ->
                                   Sorted mys (rmdup L).
 Proof.
   intros n L.
@@ -1064,7 +1064,7 @@ Theorem sorting : forall {n} (L : list (fin n * nat)),
                     {L' | StronglySorted mys L' /\ forall x, In x L <-> In x L'}.
   Proof.
     intros n L.
-    assert (xL : {L' | (forall x, In x L <-> In x L') /\ Sorted (fun x y => ((x = y) + (mys x y))%type) L'}).
+    assert (xL : {L' | (forall x, In x L <-> In x L') /\ Sorted (fun x y => ((x = y) \/ (mys x y))%type) L'}).
     apply Quicksort.quicksort.
     intros a b.
 
@@ -1073,15 +1073,15 @@ Theorem sorting : forall {n} (L : list (fin n * nat)),
     elim eq_mysab.
     intros a_eq_b.
     apply left.
-    apply inl.
+    apply or_introl.
     apply a_eq_b.
     intros mysab.
     apply left.
-    apply inr.
+    apply or_intror.
     apply mysab.
     intros mysba.
     apply right.
-    apply inr.
+    apply or_intror.
     apply mysba.
 
     elim xL.
diff --git a/Prefix.v b/Prefix.v
index f5b935e..439d3a8 100644
--- a/Prefix.v
+++ b/Prefix.v
@@ -158,94 +158,32 @@ Lemma prefix_common : forall a b c, prefix a c -> prefix b c ->
 Proof.
   refine (fix pc a b c ac bc :=
             match (a, b, c) as A return ((a, b, c) = A -> _) with
-              | (nil, b, _) => fun eq => _
+              | (nil, _, _) => fun eq => _
               | (xa :: xA, nil, _) => fun eq => _
-              | (xa :: nil, xb :: xB, _) => fun eq => _
-              | (xa :: ya :: xA, xb :: nil, _) => fun eq => _
-              | (xa :: ya :: xA, xb :: yb :: xB, nil) => fun eq => _
-              | (xa :: ya :: xA, xb :: yb :: xB, xc :: nil) => fun eq => _
-              | (xa :: ya :: xA, xb :: yb :: xB, xc :: yc :: xC) => fun eq => _
+              | (xa :: xA, xb :: xB, nil) => fun eq => _
+              | (xa :: xA, xb :: xB, xc :: xC) => fun eq => _
             end eq_refl).
+
   inversion eq.
   apply inl.
   exists b.
   auto.
-  inversion eq.
-  apply inr.
-  exists (xa :: Bnil).
-  apply app_nil_l.
 
   inversion eq.
-  apply inl.
-  exists xB.
-  inversion ac.
-  inversion bc.
-
-  rewrite <- H3 in H.
-  rewrite -> H0 in H.
-  rewrite -> H1 in H.
-  inversion H.
-  reflexivity.
-
   apply inr.
-  inversion eq.
-  exists (xa :: b0 :: l2).
+  exists (xa :: xA).
   apply app_nil_l.
 
-  inversion eq.
-  apply inr.
-  inversion ac.
-  inversion bc.
-  rewrite <- H3 in H.
-  rewrite -> H0 in H.
-  rewrite -> H1 in H.
-  inversion H.
-  exists (ya :: xA).
-  reflexivity.
-
-  inversion eq.
-  inversion ac.
-  rewrite -> H0 in H.
-  rewrite -> H2 in H.
-  inversion H.
-  inversion eq.
-  inversion ac.
-  rewrite -> H2 in H.
-  rewrite -> H0 in H.
-  inversion H.
+  exfalso.
+  inversion eq. subst.
+  eapply prefix_nnil; eauto.
 
-  inversion eq.
+  inversion eq. subst.
+  assert (xa = xc).
+  { destruct ac as (xA',ac). simpl in *. now injection ac. }
+  assert (xb = xc).
+  { destruct bc as (xB',bc). simpl in *. now injection bc. }
   assert (rec : prefix xA xB + prefix xB xA).
-  apply pc with xC.
-  inversion ac.
-  rewrite -> H0 in H.
-  rewrite -> H2 in H.
-  inversion H.
-  exists x.
-  reflexivity.
-  inversion bc.
-  rewrite -> H1 in H.
-  rewrite -> H2 in H.
-  inversion H.
-  exists x.
-  reflexivity.
-  inversion ac.
-  inversion bc.
-  rewrite <- H3 in H.
-  rewrite -> H0 in H.
-  rewrite -> H1 in H.
-  inversion H.
-  elim rec.
-  intros preab.
-  apply inl.
-  inversion preab.
-  exists x1.
-  rewrite <- H4.
-  reflexivity.
-  intros preba.
-  apply inr.
-  inversion preba.
-  exists x1.
-  rewrite <- H4.
-  reflexivity.
-Defined.
\ No newline at end of file
+  { apply pc with xC; eapply prefix_cdr; eauto. }
+  destruct rec; [left|right]; subst; now apply prefix_cons.
+Defined.
diff --git a/deflate.v b/deflate.v
index 88eab20..e6dbd4c 100644
--- a/deflate.v
+++ b/deflate.v
@@ -47,6 +47,8 @@ Defined.
 
 Definition fc1 := to_list (n:=(M (proj1_sig fixed_code))) (C (proj1_sig fixed_code)).
 
+Extraction "fc1.ml" fc1.
+
 Extraction Language Haskell.
 
 Recursive Extraction fc1. (* Fails *)