CODEWITHSUNDEEP
typescoqagdacoq-tacticinduction
user5775230
user5775230

Reputation:

How do define a custom induction principle in coq?

This is kind of a follow up on a previous question I asked, but now I'm just trying to implement my own induction principle for the equality type, which I'm not sure how to do without some kind of pattern matching. I'm avoiding using the induction tactic in the below definition, as this obviously leads to a kind of chicken vs. egg conundrum. Is there any possible way to do this with some basic tactics except indction, as well as via the vanilla Definition J2 := ...?

(* define a similair induction principle from this agda code*)
J2 : {A : Set} → (D : (x y : A) → (I A x y) →  Set)
  →  (d : (a : A) → (D a a r )) → (x y : A) → (p : I A x y) → D x y p
J2 D d x .x r = d x

Theorem J2 {A} :
  forall (D : forall (x y : A), Id A x y -> Prop), 
  forall (d : forall (a : A), (D a a (refl A a))),
  forall (x y : A) (p : Id A x y), D x y p.
Proof.
  intros.
  inversion p.
  subst.
  apply D y.

This yields the following error, and I'm not sure how to indicate that p must be a refl without the induction tactic.

1 subgoal (ID 34)

  A : Type
  D : forall x y : A, Id A x y -> Prop
  d : forall a : A, D a a (refl A a)
  y : A
  p : Id A y y
  ============================
  D y y p

Which yields the following error.

Error:
In environment
A : Type
D : forall x y : A, Id A x y -> Prop
d : forall a : A, D a a (refl A a)
y : A
p : Id A y y
Unable to unify "D y y (refl A y)" with "D y y p".

Finally, a somewhat adjoint error, when I try writing apply d in y I get the following error.

Error:
Unable to apply lemma of type "forall a : A, D a a (refl A a)"
on hypothesis of type "A".

Why isn't the typechecker happy?

Upvotes: 3

Views: 356

Answers (2)

Anton Trunov
Anton Trunov

Reputation: 15404

Is there any possible way to do this with some basic tactics except indction, as well as via the vanilla Definition J2 := ...?

Let me answer to the second part of your question:

Inductive Id (A : Type) (x : A) : A -> Type :=
  | refl : Id A x x.

Definition J2 {A} :
  forall
    (D : forall (x y : A), Id A x y -> Prop)
    (d : forall (a : A), (D a a (refl A a)))
    (x y : A) (p : Id A x y),
    D x y p
:=
  fun D d x y p =>
    match p in Id _ _ y
            return D x y p
    with
    | refl _ _ => d x
    end.

Upvotes: 2

Li-yao Xia
Li-yao Xia

Reputation: 33429

Instead of inversion p, use destruct p, which does pattern-matching in a straightforward way.

inversion is only meant to work on assumptions whose proof terms are not used in the goal. Here p is used in the goal.

Upvotes: 2

Related Questions