Coq: trying to use dependent induction

user_343123 0
Viewed 98

I have the following definitions for type precision:

Require Import Coq.Program.Equality.

Inductive type : Set :=
| TInt
| TFun: type -> type -> type
| TStar
.

Reserved Infix "<|" (at level 80).

(* Inductive TPrecision : type -> type -> Prop := *)
Inductive TPrecision : type -> type -> Type :=   (* see below *)
| PRInt : TInt <| TInt
| PRFun : forall t1 t2 t1' t2',
    t1 <| t2 -> t1' <| t2' -> TFun t1 t1' <| TFun t2 t2'
| PRStar : forall t, t <| TStar

  where "x '<|' y" := (TPrecision x y).

I want to prove that proofs of "x <| y" are unique:

Lemma TP_unique: forall t1 t2 (P1 P2 : t1 <| t2), P1 = P2.

With the previous definition of TPrecision, resulting in a Type, I can prove the lemma:

Proof.
  intros.
  dependent induction P1; dependent destruction P2; trivial.
  f_equal; auto.
Qed.

However, with the "correct" definition for TPrecision, using Prop, the tactic "dependent induction" does not work, giving the following error:

Cannot infer this placeholder of type
"DependentEliminationPackage (t1 <| t2)" (no type class instance found) in
environment:
t1, t2 : type
P1 : t1 <| t2

How to provide this missing instance? (Or how to prove that lemma another way?) If I use only "induction", instead of "dependent induction", the tactic does not type-check. I also tried stating the lemma with JMeq instead of regular equality, but it didn't work either.

dependent-type coq
1 Answers

The issue is that, by default, Coq does not generate dependent induction principles for propositions. We can fix this by overriding this default:

Require Import Coq.Program.Equality.

Inductive type : Set :=
| TInt
| TFun: type -> type -> type
| TStar
.

Reserved Infix "<|" (at level 80).

(* Ensure Coq does not generate TPrecision_ind when processing this definition *)
Unset Elimination Schemes.
Inductive TPrecision : type -> type -> Prop :=   (* see below *)
| PRInt : TInt <| TInt
| PRFun : forall t1 t2 t1' t2',
    t1 <| t2 -> t1' <| t2' -> TFun t1 t1' <| TFun t2 t2'
| PRStar : forall t, t <| TStar

  where "x '<|' y" := (TPrecision x y).
(* Re-enable automatic generation *)
Set Elimination Schemes.

(* Compare the following induction principle with the one generated by Coq by
default. *)
Scheme TPrecision_ind := Induction for TPrecision Sort Prop.

Lemma TP_unique: forall t1 t2 (P1 P2 : t1 <| t2), P1 = P2.
Proof.
  intros.
  dependent induction P1; dependent destruction P2; trivial.
  f_equal; auto.
Qed.
user_16337700
Related