See https://coq.inria.fr/doc/v8.18/refman/language/core/inductive.html
search for "Example: Non strictly positive occurrence"
Trying to reproduce the example fails:
Parameter A: Type.
Parameter a:A.
Axiom introA: ((A->Prop)->Prop) -> A.
Definition f (x: A->Prop):A := introA (fun z => z=x).
Lemma f_inj: forall x y, f x = f y -> x = y.
Proof.
Fail unfold f; intros ? ? H; injection H.
(**
The command has indeed failed with message:
Nothing to inject.
**)
Abort.
(* Here is the rest of the proof script from the manual:
set (F := fun z => z = y); intro HF.
symmetry; replace (y = x) with (F y).
+ unfold F; reflexivity.
+ rewrite <- HF; reflexivity.
Qed.
*)
Lemma f_inj: forall x y, f x = f y -> x = y.
Proof.
unfold f.
(**
============================
forall x y : A -> Prop,
introA (fun z : A -> Prop => z = x) = introA (fun z : A -> Prop => z = y) ->
x = y
**)
intros ? ? H.
(**
x, y : A -> Prop
H : introA (fun z : A -> Prop => z = x) =
introA (fun z : A -> Prop => z = y)
============================
x = y
**)
Fail injection H.
(**
The command has indeed failed with message:
Nothing to inject.
**)
Abort.
What's happening? Is the example in the manual faulty?
the manual does
#[bypass_check(positivity)] Inductive A: Type := introA: ((A -> Prop) -> Prop) -> A.
before defining f
but hides it for some reason
Thanks Gaetan. The code in the manual worked when I used your line for Inductive A.
I used the link at the top of the page to look at the source on GitHub. They should have put a \ in front of the # and maybe also before the [ and the ].
the # is not why it's hidden, it's hidden because it says coqtop:: none
I see SkySkimmer unhid this and similar code 2 days ago!
Last updated: Oct 13 2024 at 01:02 UTC