James Wood (Mar 07 2022 at 14:10): 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.
Assume I actually want to use b and c in place of exact True. and exact False..
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).
Cheers!
Notification Bot (Mar 07 2022 at 15:04):James Wood has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC