0
$\begingroup$

I have reduced my development into the following minimal reproducer:

From Coq Require Import Lists.List. Import ListNotations.
From Coq Require Import Program.Tactics.
From Coq Require Import Program.Wf.
From Coq Require Import ZArith.
From Coq Require Import Lia.
Set Default Goal Selector "!".

Inductive segment := Repeat (xs : list nat) | Symbol (x : nat).

Definition strip_sym_prefix (s : list nat) (u : list segment)
    : {u' | u = map Symbol s ++ u'} + {True}.
Admitted.

Lemma length_gt0_if_not_nil : forall A (xs : list A),
  [] <> xs -> length xs <> 0.
Proof. intros A xs H Hlen. apply length_zero_iff_nil in Hlen. auto. Qed.

Local Ltac Zify.zify_pre_hook ::=
  lazymatch goal with
  | H: [] = _ -> False |- _ => apply length_gt0_if_not_nil in H
  | _ => idtac
  end.

Local Obligation Tactic := program_simplify; autorewrite with list; intuition.

Program Fixpoint subsumes (t : list segment) (u : list segment)
    {measure (length t + length u)} : bool :=
  match u with
  | Repeat s :: u =>
    match s with
    | [] => subsumes t u
    | _ =>
      match strip_sym_prefix s t with
      | inleft (exist _ t' _) => subsumes t' (Repeat s :: u)
      | inright _ => false
      end
    end
  | _ => false
  end.

Now, Print Assumptions subsumes. only lists strip_sym_prefix as an axiom, as I would expect. However, if we run coqchk:

$ coqc --version
The Coq Proof Assistant, version 8.16.1
compiled with OCaml 4.14.0
$ coqc Repro.v
$ coqchk -silent -o -norec Repro.vo

CONTEXT SUMMARY
===============

* Theory: Set is predicative

* Axioms:
    Coq.ssr.ssrunder.Under_rel.Over_rel
    Coq.ssr.ssrunder.Under_rel.Under_rel_from_rel
    Coq.ssr.ssrunder.Under_rel.over_rel
    Coq.Logic.FunctionalExtensionality.functional_extensionality_dep
    Coq.ssr.ssrunder.Under_rel.over_rel_done
    Coq.ssr.ssrunder.Under_rel.Under_rel
    Coq.ssr.ssrunder.Under_rel.Under_relE
    Repro.strip_sym_prefix
    Repro.temporary_proof2_subproof                        <-- ???
    Coq.ssr.ssrunder.Under_rel.under_rel_done

* Constants/Inductives relying on type-in-type: <none>

* Constants/Inductives relying on unsafe (co)fixpoints: <none>

* Inductives whose positivity is assumed: <none>

As you can see, there is a stray axiom called temporary_proof2_subproof:

temporary_proof2_subproof
     : forall (s : list nat) (t' : list segment),
       ([] = s -> False) -> length t' < length s + length t'

Apart from coqchk, the extraction mechanism complains about it when I try to extract subsumes.

Some observations:

  • the axiom can be proven by lia.

  • I can make the superfluous axiom disappear, if instead of

    Local Obligation Tactic := program_simplify; autorewrite with list; intuition.
    

    I set the obligation tactic to idtac and then apply the above to each obligation manually:

    Obligation 1. program_simplify; autorewrite with list; intuition. Qed.
    Obligation 2. program_simplify; autorewrite with list; intuition. Qed.
    Obligation 3. program_simplify; autorewrite with list; intuition. Qed.
    Obligation 4. program_simplify; autorewrite with list; intuition. Qed.
    Obligation 5. program_simplify; autorewrite with list; intuition. Qed.
    Obligation 6. program_simplify; autorewrite with list; intuition. Qed.
    

To me at least, this is very surprising behavior. I do not understand what is going on. Is it a bug? How can I eliminate this axiom from my proof?

$\endgroup$
4
  • $\begingroup$ This seems exactly github.com/coq/coq/issues/13324. $\endgroup$ Sep 7, 2023 at 13:39
  • $\begingroup$ If that's correct, you should be able to use program_simplify; autorewrite with list; intuition. as Obligation Tactic, or just run Solve All Obligations with (program_simplify; autorewrite with list; intuition). $\endgroup$ Sep 7, 2023 at 13:41
  • $\begingroup$ @Blaisorblade Note that I already set this as the Obligation Tactic (just above Program Fixpoint subsumes). $\endgroup$
    – Maya
    Sep 7, 2023 at 13:58
  • $\begingroup$ @Blaisorblade it seems that this issue reports a prevalent phenomenon. On the other hand, in my development, of 4000 LoC and with hundreds of obligations, there is only one such weird subproof. $\endgroup$
    – Maya
    Sep 7, 2023 at 14:00

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.