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
    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
    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
    Jun 12, 2022 at 11:40

Your Answer

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

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