# Why does Program Fixpoint leave behind a temporary_proof2_subproof axiom in this example?

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}.

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?

• This seems exactly github.com/coq/coq/issues/13324. Sep 7, 2023 at 13:39
• 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). Sep 7, 2023 at 13:41
• @Blaisorblade Note that I already set this as the Obligation Tactic (just above Program Fixpoint subsumes).
– Maya
Sep 7, 2023 at 13:58
• @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.
– Maya
Sep 7, 2023 at 14:00