Stream: Coq users

Topic: ✔ Simultaneous set/remember


view this post on Zulip James Wood (Mar 07 2022 at 14:10):

Can I make the definition foo in-line in Ltac, i.e, without the auxiliary definition abstracted? I think it relies on a simultaneous version of set or rewrite, otherwise things become ill typed (see one example with the aborted foo' definition).

Parameter B : bool -> Type.
Parameter C : forall a, B a -> Type.

Parameter f : bool -> bool.
Parameter g : forall a, B a -> B (f a).

Lemma abstracted (fa : bool) (gab : B fa) (c : C fa gab) : Type.
  destruct fa. (* arbitrary *)
  - exact True.
  - exact False.
Defined.

Definition foo a b (c : C (f a) (g a b)) : Type := abstracted (f a) (g a b) c.

Definition foo' a b (c : C (f a) (g a b)) : Type.
  set (gab := g a b) in *.
  set (fa := f a) in *.
  Fail destruct fa.
Abort.

view this post on Zulip James Wood (Mar 07 2022 at 14:13):

Assume I actually want to use b and c in place of exact True. and exact False..

view this post on Zulip Li-yao (Mar 07 2022 at 14:48):

Definition foo' a b (c : C (f a) (g a b)) : Type.
Proof.
  revert c. generalize (g a b). destruct (f a).

view this post on Zulip James Wood (Mar 07 2022 at 15:04):

Cheers!

view this post on Zulip Notification Bot (Mar 07 2022 at 15:04):

James Wood has marked this topic as resolved.


Last updated: Feb 04 2023 at 21:02 UTC