Induction on a datatype with non-uniform type parameters produces ill-typed terms

Question

I'm working towards formalising Free Selective Applicative Functors in Coq, but struggling with proofs by induction for inductive data types with non-uniform type parameters.

Let me give a bit of an introduction on the datatype I'm dealing with. In Haskell, we encode Free Selective Functors as a GADT:

data Select f a where
    Pure   :: a -> Select f a
    Select :: Select f (Either a b) -> f (a -> b) -> Select f b

The crucial thing here is the existential type variable b in the second data constructor.

We can translate this definition to Coq:

Inductive Select (F : Type -> Type) (A : Set) : Set :=
    Pure   : A -> Select F A
  | MkSelect : forall (B : Set), Select F (B + A) -> F (B -> A) -> Select F A.

As a side note, I use the -impredicative-set option to encode it.

Coq generates the following induction principle for this datatype:

Select_ind :
  forall (F : Type -> Type) (P : forall A : Set, Select F A -> Prop),
  (forall (A : Set) (a : A), P A (Pure a)) ->
  (forall (A B : Set) (s : Select F (B + A)), P (B + A)%type s ->
     forall f0 : F (B -> A), P A (MkSelect s f0)) ->
  forall (A : Set) (s : Select F A), P A s

Here, the interesting bit is the predicate P : forall A : Set, Select F A -> Prop which is parametrised not only in the expression, but also in the expressions type parameter. As I understand, the induction principle has this particular form because of the first argument of the MkSelect constructor of type Select F (B + A).

Now, I would like to prove statements like the third Applicative law for the defined datatype:

Theorem Select_Applicative_law3
        `{FunctorLaws F} :
  forall (A B : Set) (u : Select F (A -> B)) (y : A),
  u <*> pure y = pure (fun f => f y) <*> u.

Which involve values of type Select F (A -> B), i.e. expressions containing functions. However, calling induction on variables of such types produces ill-typed terms. Consider an oversimplified example of an equality that can be trivially proved by reflexivity, but can't be proved using induction:

Lemma Select_induction_fail `{Functor F} :
  forall (A B : Set) (a : A) (x : Select F (A -> B)),
    Select_map (fun f => f a) x = Select_map (fun f => f a) x.
Proof.
  induction x.

Coq complains with the error:

Error: Abstracting over the terms "P" and "x" leads to a term
fun (P0 : Set) (x0 : Select F P0) =>
  Select_map (fun f : P0 => f a) x0 = Select_map (fun f : P0 => f a) x0
which is ill-typed.
Reason is: Illegal application (Non-functional construction):
The expression "f" of type "P0" cannot be applied to the term
 "a" : "A"

Here, Coq can't construct the predicate abstracted over the type variable because the reversed function application from the statement becomes ill-typed.

My question is, how do I use induction on my datatype? I can't see a way how to modify the induction principle in such a way so the predicate would not abstract the type. I tried to use dependent induction, but it has been producing inductive hypothesis constrained by equalities similar to (A -> B -> C) = (X + (A -> B -> C)) which I think would not be possible to instantiate.

Please see the complete example on GitHub: https://github.com/tuura/selective-theory-coq/blob/impredicative-set/src/Control/Selective/RigidImpredSetMinimal.v

UPDATE: Following the discussio in the gist I have tried to carry out proofs by induction on depth of expression. Unfortunately, this path was not very fruitful since the induction hypothesis I get in theorems similar to Select_Applicative_law3 appear to be unusable. I will leave this problem for now and will give it a try later.

Li-yao, many thanks again for helping me to improve my understanding!

Answer 1

Proofs by induction are motivated by recursive definitions. So to know what to apply induction to, look for Fixpoints.

Your Fixpoints most likely work on terms indexed by single type variables Select F A, that's exactly where you want to use induction, not at the toplevel of the goal.

A Fixpoint on terms indexed by function types A -> B is useless since no subterms of any Select term are indexed by function types. For the same reason, induction is useless on such terms.

Here I think the strong type discipline actually forces you to work everything out on paper before trying to do anything in Coq (which is a good thing in my opinion). Try to do the proof on paper, without even worrying about types; explicitly write down the predicate(s) you want to prove by induction. Here's a template to see what I mean:

By induction on u, we will show

 u <*> pure x = pure (fun f => f x) <*> u

    (* Dummy induction predicate for the sake of example. *)
    (* Find the right one. *)
    (* It may use quantifiers... *)

1. Base case (set u = Pure f). Prove:

   Pure f <*> pure x = pure (fun f => f x) <*> Pure f
   

2. Induction step (set u = MkSelect v h). Prove:

   MkSelect v h <*> pure x = pure (fun f => f x) <*> MkSelect v h
   

   assuming the induction hypothesis for the subterm v (set u = v):

   v <*> pure x = pure (fun f => f x) <*> v
   

Notice in particular that the last equation is ill-typed, but you can still run along with it to do equational reasoning. Regardless, it will likely turn out that there is no way to apply that hypothesis after simplifying the goal.

---

If you really need to use Coq to do some exploration, there is a trick, consisting in erasing the problematic type parameter (and all terms that depend on it). Depending on your familiarity with Coq, this tip may turn out to be more confusing than anything. So be careful.

The terms will still have the same recursive structure. Keep in mind that the proof should also follow the same structure, because the point is to add more types on top afterwards, so you should avoid shortcuts that rely on the lack of types if you can.

(* Replace all A and B by unit. *)
Inductive Select_ (F : unit -> Type) : Set :=
| Pure_ : unit -> Select_ F
| MkSelect_ : Select_ F -> F tt -> Select_ F
.

Arguments Pure_ {F}.
Arguments MkSelect_ {F}.

(* Example translating Select_map. The Functor f constraint gets replaced with a dummy function argument. *)
                                        (*      forall A B, (A -> B) -> (F A -> F B) *)
Fixpoint Select_map_ {F : unit -> Type} (fmap : forall t,   unit     -> (F t -> F t)) (f : unit -> unit) (v : Select_ F) : Select_ F :=
  match v with
  | Pure_ a => Pure_ (f a)
  | MkSelect_ w h => MkSelect_ (Select_map_ fmap f w) (fmap _ tt h)
  end.

With that, you can try to prove this trimmed down version of the functor laws for example:

Select_map_ fmap f (Select_map_ fmap g v) = Select_map_ fmap (fun x => f (g x)) v

(* Original theorem:

Select_map f (Select_map g v) = Select_map (fun x => f (g x)) v

*)

The point is that removing the parameter avoids the associated typing problems, so you can try to use induction naively to see how things (don't) work out.