trivial theorem about my inductive type on Coq

user_10622059 0
Viewed 155

I defined the dependent type and trivial lemma as you can see below.

Require Import Coq.Reals.Reals.

Inductive Euc :nat -> Type:=
|RO : Euc 0
|Rn : forall {n:nat}, R -> Euc n -> Euc (S n).

Lemma ROEuc : forall t:(Euc 0), t = RO.
Proof.
intros. Admitted.

I don't know how to prove it. Euc 0 is not an inductive type, so I can not use destruct t or induction t.

Please tell me how to prove it.

coq
2 Answers

You should find it easy to prove the more simply-typed theorem

Lemma ROEuc' : forall n (t : Euc n), n = 0 -> existT Euc n t = existT Euc 0 RO.

You can simply destruct t, giving you one trivial case, and one absurd case that can be discharged with congruence.

To derive your lemma from this one, you will need four tools:

  1. The inversion_sigma tactic to turn an equality of existT s into dependent equalities
  2. The fact UIP_dec from Coq.Logic.Eqdep_dec to prove that all proofs of 0 = 0 are equal to eq_refl under the assumption that equality of nat is decidable
  3. The fact that equality of nat is decidable, which you can either take from some lemma in Coq.Arith.Arith (use Search after Require Import Coq.Arith.Arith to find the name of the lemma with the right type) or prove from scratch using the decide equality tactic
  4. subst + simpl to see that your dependent equality will now reduce to the theorem you want to prove

Alternatively, you can Require Import Coq.Program.Tactics and use dependent destruction t, but beware that this often introduces needless dependencies on axioms (visible with Print Assumptions)

user_3770220

In this case, Coq is actually smart enough to do the dependent pattern matching for you. The magic tactic to use here is refine (match t in Euc 0 with RO => _), which leaves you with a single trivial goal (there may be a variant of destruct that does this, but I don't know what it would be). Here the clause in Euc 0 tells Coq that you are only interested in 0-length vectors, and since 0 is a nat built from constructors, Coq is able to work out that the RS case is impossible by disjointness of constructors.

The full proof:

Lemma ROEuc : forall t:(Euc 0), t = RO.
Proof.
intros.
refine (match t in Euc 0 with RO => _ end).
reflexivity.
Qed.

The proof term generated by this match is actually rather complicated, but understanding it might be helpful if you need to write other proofs about dependent types where Coq's pattern matching isn't powerful enough to help you.

user_26443680
Related