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 https://coq.inria.fr/doc/V8.8.2/refman/proof-engine/tactics.html#coq:tacn.admit

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: https://coq.inria.fr/doc/V8.19.0/refman/proofs/writing-proofs/proof-mode.html#coq:tacn.admit

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

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):

btw

Axiom oops : False.

Axiom T : Prop.

Lemma foo : T.
  case oops.
Qed.

Print Assumptions foo.
(*
Axioms:
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