## Stream: Coq users

### Topic: Non strictly positive occurrence exampl, COQManual problem?

#### Seth Chaiken (Nov 09 2023 at 19:45):

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?

#### Gaëtan Gilbert (Nov 09 2023 at 19:54):

the manual does

``````      #[bypass_check(positivity)] Inductive A: Type := introA: ((A -> Prop) -> Prop) -> A.
``````

before defining `f` but hides it for some reason

#### Seth Chaiken (Nov 09 2023 at 22:28):

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 ].

#### Gaëtan Gilbert (Nov 09 2023 at 23:28):

the # is not why it's hidden, it's hidden because it says `coqtop:: none`

#### Seth Chaiken (Nov 12 2023 at 04:27):

I see SkySkimmer unhid this and similar code 2 days ago!

Last updated: Jun 22 2024 at 16:02 UTC