This is a follow-up for Li-yao Xia's answer on my StackOverflow question
Thanks for your answer Li-yao! I have a couple of follow-up notes/questions:
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.
The reason I wanted to do induction on a term of type Select F (A -> B) in the first place is because I have been drawing inspiration from proofs of Applciative laws for other structures, specifically lists and free applicative functors. Consider the proof of this property for lists (adopted from John Wiegley's coq-haskell library):
Theorem List_Applicative_law3 :
forall (A B : Set) (u : list (A -> B)) (y : A), u <*> pure y = pure ((fun f => f y)) <*> u.
Proof.
simpl.
induction u; simpl; trivial; intros.
now rewrite IHu.
Qed.
Here, we induct on (u : list (A -> B) without any issues since the list's constructors do not have type indices and therefore the predicate in its eliminator is only quantified by a term, not by a type.
In the Free Applicative Functors paper, Capriotti and Kaposi suggest the following datatype and provide pen-and-paper proofs that it is a lawful applicative functor:
data FreeA f a = Pure a
| ∀b . MkAp (f (b → a)) (FreeA f b)
Which I encoded in Coq in the following way:
Inductive FreeA (F : Type -> Type) (A : Set) :=
Pure : A -> FreeA F A
| MkAp : forall (B : Set), F (B -> A) -> FreeA F B -> FreeA F A.
This type is similar to my Select since its second constructor is also indexed by a type variable and thus the predicate in the eliminator becomes quantified in this type variable.
To prove the third applicative law (see Lemma 3 on page 16), the authors perform induction
on a term of type Free F (A -> B). However, when I have tried to formalize their proofs in Coq,
I failed for exactly the same reason that in the case of Select. The authors have reported a failed attempt to formalize the proofs in Agda, but they do not go into much detail why they failed. I will probably contact them about it at some point.
These two examples make me convinced that I'm going in the right direction with wanting to do induction on terms of type Select F (A -> B). Even though I did find a way around doing induction on u in the particular case of the third applicative law (you may take a look at my proof here, I still want to find a way to perform an inductive proof because I'm running into the same issue in proofs of other properties and I'm almost convinced that using induction there would be inevitable.
Do you think it makes any sense? Maybe my attempts are just too naive and I need to workout some other way to formalize free selective functors which would avoid using type indices.
P. S.
I didn't mention that in my initial question, but I have three useful free theorems that hold for Select by parametricity (and thus have to be admitted as axioms), which are useful for "reshuffling" arguments of Select_select function calls and MkSelect constructors. These help to massage the goal into the required form to apply inductive hypothesis in some of my proofs, for example the one of the ap_fmap : fmap f x = pure f <*> x property.
Thanks for your detailed response, that's an interesting take!
Your proofs of law 3 that doesn't use induction on
u : Select F (A -> B)uses lemmas that do induction on termsSelect F A', so that looks like the kind of solution I was talking about.Induction on
list (A -> B)makes sense because there are only subterms of the same type in the inductive case.Selectis different in that sense.Capriotti and Kaposi's proof considers that the "structurally smaller" relation for the induction step is preserved by
fmap. That's a bigger relation than the implicit "subterm" relation in Coq and Agda, which might explain why a direct attempt would not work (they may also have run into deeper issues I haven't foreseen). To reproduce that proof, you can define that more general "structurally smaller" relation and prove it is well-founded. In fact, since you have already defined a notion of depth as the decreasing measure forFunction, which you have proved is preserved byfmap, you could use that in proofs as well to similar effect as that paper proof, by performing induction on depth.The custom ordering relation/depth measure has the benefit of being comprehensible without deep knowledge of Coq's reduction semantics, at the cost of increased verbosity (to prove the well-foundedness property and there may be some extra rewriting), which is arguably acceptable for many people.
I might give these proofs a try over the weekend...