Stream: Coq users

Topic: Definition in a proof

Callan McGill (Jan 27 2022 at 05:12):

I am trying to define something in a proof. I have the following set up:

Definition nat_rec (P : nat -> Type) (p0 : P 0) (psuc : forall n, P n -> P (S n)) (n : nat) : P n.
Proof.
  Definition
    sigsuc (p : {n | P n}) : {n | P n} :=
    match p with
    | (n ; pn) => (S n, psuc _ pn)
    end.

I get told that the reference to P was not found in the current environment, is there a different way to make something like this work (apologies I am not experienced at coq).

Guillaume Melquiond (Jan 27 2022 at 06:06):

You are looking for tactics such as pose and set: https://coq.inria.fr/distrib/current/refman/proof-engine/tactics.html#coq:tacn.pose

Callan McGill (Jan 27 2022 at 19:24):

Thank you!

Callan McGill (Jan 28 2022 at 00:36):

Could you tell me how you can add a type sig to pose or set. What I tried did not seem successful.

Li-yao (Jan 28 2022 at 01:05):

I don't know the answer but refine (let sigsuc (p : {n | P n}) : {n | P n} := (blah) in _) seems like a workaround.

Last updated: Apr 19 2024 at 16:01 UTC