3
$\begingroup$

I have a Program Fixpoint with measure for which I have proved all obligations. When I try to check it, it fails:

Error: The reference trivial_program_fixpoint2 was not found in the current environment.

I have narrowed the error to the use of a non default tactic to prove obligations. In the code below, the first Program is defined. Once I choose a non default tactic to prove Obligations, the Program doesn't get defined even though there are no Obligation's left to prove. I would expect trivial_program_fixpoint2 to be defined after Qed.

I have looked in the documentation but I don't see anything that suggests that using a tactic different than default would change what I am seeing.

Coq version used:

The Coq Proof Assistant, version 8.15+alpha compiled with OCaml 4.09.1

Below is code to reproduce the problem.

From Coq Require Export Arith.
Require Import Program.Wf.

Program Fixpoint trivial_program_fixpoint (n : nat) {measure n}: nat :=
  match n with
    0 => 0
  | m => m
  end.
Check trivial_program_fixpoint.

Obligation Tactic := intros.

Program Fixpoint trivial_program_fixpoint2 (n : nat) {measure n}: nat :=
  match n with
    0 => 0
  | m => m
  end.
Next Obligation.
  intuition. discriminate.
Qed.
Check trivial_program_fixpoint2.
Improve this question
$\endgroup$

1 Answer 1

Reset to default
3
$\begingroup$

Your second Program Fixpoint produced two obligations.

trivial_program_fixpoint2 has type-checked, generating 2 obligations

Solving obligations automatically...

2 obligations remaining
Improve this answer
$\endgroup$
3
  • $\begingroup$ Thanks. I thought Qed was used when no obligations are left. $\endgroup$
    – Roland Coeurjoly
    Commented Jun 10, 2022 at 13:42
  • 1
    $\begingroup$ @RolandCoeurjoly Qed is accepted when no goals are left. The obligations generated by Program work a little differently. I don't know why this is. One consequence is that each solved obligation becomes a defined object in its own right, and one can choose whether to close them with Defined or Qed. $\endgroup$
    – Ana Borges
    Commented Jun 10, 2022 at 15:16
  • $\begingroup$ Program is different (obligations are not generated as subgoals) because it lets you choose whether to make the obligations transparent or not. $\endgroup$
    – HTNW
    Commented Jun 12, 2022 at 11:40

Not the answer you're looking for? Browse other questions tagged or ask your own question.