Stream: Coq users

Topic: Non strictly positive occurrence exampl, COQManual problem?


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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 ].

view this post on Zulip Gaëtan Gilbert (Nov 09 2023 at 23:28):

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

view this post on Zulip Seth Chaiken (Nov 12 2023 at 04:27):

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


Last updated: Oct 13 2024 at 01:02 UTC