Can't compute value, having "?Goal" inside the term

Using Coq
1

Hello!
I can’t compute some value. This is what I get:

 = let (a, _) :=
     match ex_123_permutation_list_subproof with
     | conj H1 H2 => exist (fun i : nat => S i <= 1) 0 (plist_to_permutation_aux_subproof H1 H2 ?Goal)
     end in
   a
 : nat

What could be cause of this weird thing?

P.S. I hope I don’t ask questions to frequently… apologies if I take too much space.

2

Don’t worry about asking too many questions, its good to have more activity around here.

Now about your problem it seems that coq is not able to apply ex_123_permutation_list_subproof, probably because some match got stuck and since that definition is Opaque it will not unfold. Anyways, I would need more context to give more help.

3

There’s the context. I changed all Qed to Defined, with the same result.

Set Implicit Arguments.
Require Import Arith Omega List Bool.

Fixpoint nat_eq_bool (n m: nat): bool :=
  match n, m with
  | O, O => true
  | S n', S m' => nat_eq_bool n' m'
  | _, _ => false
  end.

(* Simplified proof by mwuttke97 from coq.discourse.group *)
Theorem nat_eq_reflect: forall n m, reflect (n = m) (nat_eq_bool n m).
Proof.
  induction n as [| n' H]; intros [| m']; simpl in *.
  + apply ReflectT. auto.
  + apply ReflectF. intuition.
  + apply ReflectF. intuition.
  + destruct (H m') as [IH | IH].
    - apply ReflectT. congruence.
    - apply ReflectF. congruence.
Defined.

Fixpoint le_bool (n m: nat): bool :=
  match n, m with
  | O, _ => true
  | S n', S m' => le_bool n' m'
  | _, _ => false
  end.
Theorem le_reflect: forall n m, reflect (n <= m) (le_bool n m).
Proof.
  induction n as [| n' H]; intros [| m']; simpl in *.
  + apply ReflectT. intuition.
  + apply ReflectT. intuition.
  + apply ReflectF. intuition.
  + destruct (H m') as [IH | IH].
    - apply ReflectT. intuition.
    - apply ReflectF. intuition.
Defined.
Definition lt_bool (n m: nat) := le_bool (S n) m.

Definition In_bool A (x: A) (L: list A) (beq: A -> A -> bool): bool.
Proof.
  induction L.
  + exact false.
  + exact (orb (beq x a) IHL).
Defined.
Theorem In_reflect A (x: A) (L: list A) (beq: A -> A -> bool) (H: forall x y, reflect (x = y) (beq x y)):
    reflect (In x L) (In_bool x L beq).
Proof.
  induction L.
  + simpl. apply ReflectF. auto.
  + simpl. destruct (H a x).
    - subst. assert (beq x x = true). destruct (H x x); auto.
      rewrite H0. simpl. apply ReflectT. left. auto.
    - destruct IHL.
      * replace (beq x a || true) with true by intuition. apply ReflectT. auto.
      * assert (beq x a = false). destruct (H x a); congruence.
        rewrite H0. simpl. apply ReflectF. tauto.
Defined.

Definition NoDup_bool A (L: list A) (beq: A -> A -> bool): bool.
Proof.
  induction L.
  + exact true.
  + exact (negb (In_bool a L beq) && IHL).
Defined.
Theorem NoDup_reflect A (L: list A) (beq: A -> A -> bool) (H: forall x y, reflect (x = y) (beq x y)):
    reflect (NoDup L) (NoDup_bool L beq).
Proof.
  induction L.
  + simpl. apply ReflectT. apply NoDup_nil.
  + simpl. destruct (In_reflect a L _ H).
    - simpl. apply ReflectF. intro. apply NoDup_cons_iff in H0. tauto.
    - simpl. destruct IHL.
      * apply ReflectT. apply NoDup_cons; auto.
      * apply ReflectF. intro. apply NoDup_cons_iff in H0. tauto.
Defined.


Theorem le_proof_irrelevance: forall n m (p q: le n m), p = q.
Admitted.

Definition fin n := { i | i < n }.
Coercion fin_to_nat n (f: fin n): nat := proj1_sig f.


Definition permutation n := { f: fin n -> fin n | forall y, exists x, f x = y }.
Definition permutation_mult n (p1 p2: permutation n): permutation n.
Proof.
  destruct p1 as [f1 H1], p2 as [f2 H2]. exists (fun x => f2 (f1 x)).
  intros. destruct (H2 y). subst. destruct (H1 x). rewrite <- H.
  exists x0. auto.
Defined.

Definition permutation_list n := { L: list nat | (forall x, In x L <-> x < n) /\ NoDup L }.
Definition permutation_list_length n (p: permutation_list n): length (proj1_sig p) = n.
Proof.
Admitted.



Theorem aux n (L: list nat): (forall x, In x L <-> x < n) <-> ((forall x, In x L -> x < n) /\ (forall x, x < n -> In x L)).
Proof.
  split; intros.
  + split; intros.
    - apply H. auto.
    - apply H. auto.
  + destruct H. split; intros.
    - apply H. auto.
    - apply H0. auto.
Defined.

Definition aux1_bool (n: nat) (L: list nat): bool.
Proof.
  induction L.
  + exact true.
  + exact (if le_bool (S a) n then IHL else false).
Defined.
Theorem aux1_reflect (n: nat) (L: list nat): reflect (forall x, In x L -> x < n) (aux1_bool n L).
Proof.
  induction L.
  + simpl. apply ReflectT. tauto.
  + simpl. destruct n.
    - apply ReflectF. intro. assert (a < 0). apply H. left. auto. inversion H0.
    - destruct (le_reflect a n).
      * destruct IHL.
        ++ apply ReflectT. intros. destruct H.
          -- subst. intuition.
          -- apply l0. auto.
        ++ apply ReflectF. intro. apply n0. intros. apply H. auto.
      * apply ReflectF. intro. apply n0. assert (a < S n).
        apply H. auto. intuition.
Defined.

(* Simplified definition by mwuttke97 from coq.discourse.group *)
Definition aux2_bool (n : nat) (L: list nat) :=
  forallb (fun x => In_bool x L nat_eq_bool) (seq 0 n).

(* Proof by mwuttke97 from coq.discourse.group *)
Lemma forallb_reflect (X : Type) (f : X -> bool) (xs : list X) :
  reflect (forall x, In x xs -> f x = true) (forallb f xs).
Proof.
  induction xs.
  - cbn. left. tauto.
  - cbn. destruct (f a) eqn:E; cbn.
    + destruct IHxs.
      * left. intros x [-> | H]; auto.
      * right. intuition.
    + right. intros H. specialize (H a (or_introl eq_refl)). congruence.
Defined.

(* Proof by mwuttke97 from coq.discourse.group *)
Theorem aux2_reflect (n: nat) (L: list nat): reflect (forall x, x < n -> In x L) (aux2_bool n L).
Proof.
  unfold aux2_bool.
  pose proof forallb_reflect (fun x => In_bool x L nat_eq_bool) (seq 0 n) as [H|H].
  - left. intros x Hx.
    assert (In x (seq 0 n)) as Haux.
    { replace x with (x + 0) by omega. apply in_seq. omega. }
    specialize H with (1 := Haux).
    rewrite reflect_iff; eauto.
    apply In_reflect. intros. apply nat_eq_reflect.
  - right. intros H'. contradict H.
    intros x Hx.
    assert (x < n) as Haux.
    { apply in_seq in Hx. omega. }
    specialize H' with (1 := Haux).
    rewrite reflect_iff in H'; eauto.
    apply In_reflect. intros. apply nat_eq_reflect.
Defined.

Theorem aux3_reflect (n: nat) (L: list nat):
    reflect ((forall x, In x L <-> x < n) /\ NoDup L) (aux1_bool n L && aux2_bool n L && NoDup_bool L nat_eq_bool).
Proof.
  destruct (aux1_reflect n L).
  + simpl. destruct (aux2_reflect n L).
    - simpl. destruct (NoDup_reflect L _ nat_eq_reflect).
      * apply ReflectT. split; auto. apply aux; auto.
      * apply ReflectF. intro. apply n0. tauto.
    - simpl. apply ReflectF. intro. apply n0. clear n0. destruct H. apply aux in H. tauto.
  + simpl. apply ReflectF. intro. apply n0. clear n0. destruct H. apply aux in H. tauto.
Defined.

Definition plist_to_permutation_aux n (pl: permutation_list n): fin n -> fin n.
Proof.
  pose (permutation_list_length pl) as H.
  intros [i H0]. destruct pl as [l [H1 H2]]. simpl in H.
  exists (nth i l 0).
  abstract (assert (In i l) by (apply H1; auto); apply H1, nth_In; rewrite H; auto).
Defined.
Theorem plist_to_permutation_aux_thm n (pl: permutation_list n): forall y, exists x, plist_to_permutation_aux pl x = y.
Proof.
Admitted.

Definition plist_to_permutation {n} (pl: permutation_list n): permutation n.
Proof.
  exists (plist_to_permutation_aux pl). apply plist_to_permutation_aux_thm.
Defined.

(* Testing plist_to_permutation *)

Definition ex_123_permutation_list: permutation_list 1.
Proof.
  pose (0::nil) as L. exists L. abstract (pose (aux3_reflect 1 L); simpl in *; inversion r; auto).
Defined.
Eval compute in proj1_sig ex_123_permutation_list.
Eval compute in proj1_sig (plist_to_permutation_aux ex_123_permutation_list (exist _ 0 ltac:(auto))).
4

Yes but you have some Admitted. which are blocking computation as well (even more somehow since Coq has no information about the content at all).

5

I think the problem comes from this definition

Definition plist_to_permutation_aux n (pl: permutation_list n): fin n -> fin n.
Proof.
  pose (permutation_list_length pl) as H.
  intros [i H0]. destruct pl as [l [H1 H2]]. simpl in H.
  exists (nth i l 0).
  abstract (assert (In i l) by (apply H1; auto); apply H1, nth_In; rewrite H; auto).
Defined.

In the second line of the proof you destruct your permutation and do a case analysis on the proof term that comes with it before providing the first component. One way to solve your problem here is to change the order of operations in your proof script so that the computational part does not depend on the proof part, something like:

Definition plist_to_permutation_aux n (pl: permutation_list n): fin n -> fin n.
Proof.
  pose (permutation_list_length pl) as H.
  intros [i H0]. destruct pl as [l H12].
  exists (nth i l 0).
  abstract (destruct H12 as [H1 H2]; assert (In i l) by (apply H1; auto); apply H1, nth_In; rewrite H; auto).
Defined.

(not tested)

1 Like