2
$\begingroup$

I'm trying to do induction on an instance of an indexed type family in Coq. Here's a simplified example:

Inductive T: Type :=
| A
| B.

Inductive P: T -> Type :=
| P1: P A
| P2: P A
| P3: P B.

Inductive R: forall {T}, P T -> P T -> Prop :=
| R1: forall (x: P A) (y: P A), R x y.

Lemma failed_attempt:
  forall (H: P A), R H P2.
Proof.
  intro.
  induction H.

I expect the induction tactic to discharge the P3 case and ask me to prove the remaining two. However, it fails with:

Error: Abstracting over the terms "t" and "H" leads to a term
fun (t0 : T) (H0 : P t0) => R H0 P2
which is ill-typed.
Reason is: Illegal application: 
The term "@R" of type "forall T : T, P T -> P T -> Prop"
cannot be applied to the terms
 "t0" : "T"
 "H0" : "P t0"
 "P2" : "P A"
The 3rd term has type "P A" which should be coercible to 
"P t0".

I realized this could be caused by Coq generalizing H: P A to H: P ?t0, which makes R H P2 an ill-typed term.

Of course, I can use dependent induction from Program, but that tactic uses JMeq. I'm quite skeptical about whether JMeq is truly necessary in this case. Is there a way to do such an induction without JMeq? And if possible, is there a better tactic to help me do this?

Update: the example I gave was oversimplified. This is what I'm actually working on: stlc.v. I believe I don't need global UIP because all types involved are inductive type and thus have decidable equality.

I'm now pretty sure I can do this without JMeq or any other axiom. Is there a way to automate specializing the inductive principle?

$\endgroup$
5
  • 1
    $\begingroup$ In your example, you do not need to use induction on H at all, constructor suffices. I guess this is unintended? Can you provide a more realistic MWE where you need induction? $\endgroup$ Commented Feb 26 at 10:02
  • $\begingroup$ @MevenLennon-Bertrand Yes, the example is oversimplified. This is what I'm actually working on: stlc.v. Pay attention to usages of dependent induction. $\endgroup$ Commented Feb 26 at 15:52
  • $\begingroup$ Do you expect to prove normalisation for stlc by a direct induction? Do you know this will not work, and you need to build a logical relation instead (which, coincidentally, will take care of the generalisation over context and type)? $\endgroup$ Commented Feb 26 at 17:59
  • 1
    $\begingroup$ @MevenLennon-Bertrand Actually, I'm trying to follow Harper's lecture notes on Tait's method, which introduces logical relation HT. I deliberately attempted the wrong proof to better understand the motivation for introducing logical relations in a non-categorical way. $\endgroup$ Commented Feb 26 at 19:04
  • 1
    $\begingroup$ So now I guess you have a good reason why it does not work: the induction does not go through because it is not general enough, as you realized yourself :) That is: the theorem, since it talks about only a specific context and a specific type, cannot be directly proven by induction. Rather, you should give a motive that is valid for all types/contexts. In Coq, this manifests as induction having difficulties coping with your goal. You can try all forms of dependent shenanigans to go around it, but they will not really help you, because the problem is deeper: the proof strategy is flawed. $\endgroup$ Commented Feb 27 at 10:18

3 Answers 3

1
$\begingroup$

You can do without because T is simple enough. Here, "simple enough" means that it has decidable equality. There are actually several ways of going about it:

(* Specialized induction principle *)
Lemma P_A_ind (motive : P A -> Prop) :
  motive P1 -> motive P2 -> forall p, motive p.
Proof.
  intros HP1 HP2 p.
  (* Idea 1, match on [t] to exclude other cases *)
  pose (motive2 := fun (t:T) (p : P t) => match t with A => fun p => motive p | _ => fun _ => True end p).
  unshelve eapply (P_ind motive2 _ _ _ A p).
  - apply HP1.
  - apply HP2.
  - easy.
Qed.

Lemma T_dec (x y : T) : {x = y} + {x <> y}.
Proof. decide equality. Defined.

(* Specialized induction principle, take 2 *)
Lemma P_A_ind_2 (motive : P A -> Prop) :
  motive P1 -> motive P2 -> forall p, motive p.
Proof.
  intros HP1 HP2 p.
  (* Idea 2, constrain t using an equality *) 
  pose (motive2 := fun (t:T) (p : P t) => forall (Heq : A = t), match Heq with eq_refl => fun p => motive p end p).
  (* We will later need that all equality proofs on A are equal to the identity.
     This holds due to Hedberg's theorem, since T has decidable equality, as proven above. *)
  assert (forall (H : A = A), H = eq_refl) as Helim.
  { intros H. eapply K_dec_type with (p := H). 1: apply T_dec. reflexivity. }
  unshelve eapply (P_ind motive2 _ _ _ A p eq_refl).
  - intros Heq.
    (* Somewhat complicated dance to use the above equality *)
    specialize (Helim Heq). subst Heq.
    apply HP1.
  - intros Heq.
    (* Alternatively, one can inline the proof that UIP holds on T here *)
    elim Heq using K_dec_type. 1: apply T_dec.
    apply HP2.
  - intros [=].
Qed.


Lemma failed_attempt:
  forall (H: P A), R H P2.
Proof.
  intros H.
  (* Just a fancy way of applying [P_A_ind] *)
  induction H using P_A_ind. (* or P_A_ind_2 *)
  - apply R1.
  - apply R1.
Qed.

(* Unlike dependent induction, this does not incur any axioms *)
Print Assumptions failed_attempt.

Decidable equality is used in P_A_ind_2, where Hedberg's theorem allows us to eliminate the proof that A = A into eq_refl to then match on it. Formally, we exploit that T has unique identity proofs. For more, see e.g. sections 1-3 of https://www.cs.nott.ac.uk/~psznk/docs/hedberg.pdf.

$\endgroup$
2
  • $\begingroup$ Recently I got some insight from this idea: indexed type family can be encoded with plain inductive types and an id type ("ford"). Therefore, P can be encoded as P (t: T) := P1: t = A -> P | P2: t = A -> P | P3: t = B -> P. To pattern match on an instance of P A, I got three cases. For case P3, we want to show (A = B) -> _, which can be solved by decidable equality and exfalso. It looks similar to your second idea but doesn't require UIP on T, which is too good to be true. Do I need UIP on T for the encoding itself to work? $\endgroup$ Commented Feb 26 at 17:30
  • 1
    $\begingroup$ No, fording is general, it should also work for types without UIP. Although the exact statement of how and when it works are I believe not entirely worked out. $\endgroup$ Commented Feb 26 at 17:54
1
$\begingroup$

If you just want to quickly decide whether it is possible, the criterion is pretty simple. For each constructor, you unify the indices of its type with the current type. There are only a few restrictions: you are not allowed to delete the equation $x = x$ where $x$ is a variable; and suppose you use the injectivity rule on $\mathsf c E_1 \dots E_n = \mathsf c F_1\dots F_n : T$, you need to first check that $T$ is unifiable with itself under our restrictions.

Here, the pattern matching on $H$ requires us to unify the current type $P \mathsf A$ with the possible type indices $P \mathsf A$ or $P \mathsf B$. Since they are made of constructors, you can use the injectivity rule and no confusion rule to solve the unification. Hence you should only be left with the case for P1 and P2, without using UIP.

$\endgroup$
2
  • $\begingroup$ Is this the unification algorithm for type index? $\endgroup$ Commented Feb 26 at 17:54
  • 2
    $\begingroup$ @LightQuantum This is the "correct" algorithm for elaborating dependent pattern matching. It is implemented in Agda --without-K, for example. Although Agda does not translate this to eliminators; rather it just checks the criterion. $\endgroup$
    – Trebor
    Commented Feb 26 at 18:33
1
$\begingroup$

In your case, $P$ is just a type family indexed by $T$ and when you are case splitting a term $P A$, you are trying to unify the index of all possible $T$ which yields a substitution so that $T = A$. Since $T$ is just a simple type built from constructors, the unification will never result in a failure thanks to injectivity. Coq can analyze $T = A$ and discharges two cases $P_1$ and $P_2$.

To see why unification succeeds in this case without UIP, you can check Agda's implementation on how --without-K is achieved.

If UIP is needed, you want to delete $x = x$, which is unnecessary in your case because injectivity suffices to solve the goal, and $T$ is fairly a simple type.

Lemma failed_attempt:
  forall (H: P A), R H P2.
Proof.
  intro.
  constructor.
Qed.
$\endgroup$
5
  • $\begingroup$ The example I gave in this question was oversimplified. For my original problem, I need to use inductive reasoning. I'm pretty sure I still don't need global UIP since I only have inductive types. The issue is that Coq's induction tactic seems to be too weak and cannot handle index unification for me. $\endgroup$ Commented Feb 26 at 17:41
  • 1
    $\begingroup$ The rule you described is too strong and famously leads to a variant of UIP being provable: you can pattern match on p : refl = refl since refl is a constructor, and using injectivity you are allowed to conclude that p = refl. This is not provable in MLTT without UIP, by the 2-groupoid model. $\endgroup$
    – Trebor
    Commented Feb 26 at 18:31
  • $\begingroup$ @Trebor I see, you are right. The criteria indeed implies somehow a weaker notion of K. I've made the correction. $\endgroup$ Commented Feb 26 at 18:51
  • $\begingroup$ @LightQuantum It seems that refine (match M with ... end) works here but I am also surprised by the fact that induction cannot automatically do this for us. $\endgroup$ Commented Feb 26 at 19:07
  • $\begingroup$ @LightQuantum For what it is worth, proofassistants.stackexchange.com/a/1248/3186 this answer might also help $\endgroup$ Commented Feb 26 at 19:16

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.