The Coq mailing list

[Clément Pit-Claudel <cpitclaudel AT gmail.com>]

On 8/21/21 5:01 PM, Marco Servetto wrote:
> Dear List, I'm trying to model a problem in COQ but I got stuck. My
> minimized problem is the following:
> 
>     Inductive Bool : Type :=  | T | F.
>     Inductive A : Type :=
>       | myA : (A->Bool)->A.

You minimized the problem too far, and Coq's concern with this type is 
legitimate.  The problem is that this definition would let you build 
non-terminating functions, and from there prove False.  

Let's see how the problem manifests itself.  Start by turning off the 
positivity checker for a moment:

  Unset Positivity Checking.
  Inductive A : Type := myA : (A -> Bool) -> A.
  Set Positivity Checking.

Then define this fine function:

  Definition not (b: Bool) :=
    match b with T => F | F => T end.

And this odd one:

  Definition loopy (a: A) :=
    match a with myA f => not (f a) end.

That's enough; the following never terminates:

  Compute (loopy (myA loopy)).

And indeed:

  Goal False.
    pose (loopy (myA loopy)) as b.

      b := loopy (myA loopy): Bool
      ----------------------------
      False

    assert (b = not b) by reflexivity.

      b := loopy (myA loopy): Bool
      H: b = not b
      ----------------------------
      False

    destruct b; discriminate.
  Qed.

There's a bit more detail on this in Chapter 3.6 "Reflexive Types" of CPDT.

Clément.