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?

Look at https://coq.inria.fr/doc/V8.8.2/refman/proof-engine/tactics.html#coq:tacn.admit

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

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.

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