Stream: Coq users

Topic: Admit a sub-goal in a proof

view this post on Zulip Julin Shaji (Apr 20 2024 at 15:54):

While doing a proof, is there a way to admit only the current sub-goal?
Instead of admitting the whole proof?

Or is the way to do that shelving the sub-goal and admit when all other goals are done?

view this post on Zulip Quentin VERMANDE (Apr 20 2024 at 16:22):

Look at

view this post on Zulip Ali Caglayan (Apr 23 2024 at 19:29):

That link is a bit old, here is the 8.19 manual:

view this post on Zulip Ali Caglayan (Apr 23 2024 at 19:34):

There are situations where you want Admitted to be transparent, say there is a case you haven't handled yet in your function you want to prove something about. In that case you can create a custom admit tactic like:

  Axiom oops : False.
  Ltac sorry := apply (False_rect (fun _ => _) oops).

  Goal False.

This let's you prove anything. Just don't forget to remove it after experimenting.

view this post on Zulip Gaëtan Gilbert (Apr 23 2024 at 19:49):


Axiom oops : False.

Axiom T : Prop.

Lemma foo : T.
  case oops.

Print Assumptions foo.
oops : False
 used in foo to prove: T

(apply False_rect and destruct oops seem to generate too complex terms for the "used in foo to prove" heuristic to understand them)

Last updated: Jun 23 2024 at 04:03 UTC