CODEWITHSUNDEEP
coq
user2833557
user2833557

Reputation: 677

How to use matched case and variable equivalence in coq

I am trying to use the following theorem

Theorem nat_rect_1_2: forall (P:nat->Type), (P O -> P 1 
  -> (forall n:nat, P n -> P (S n) -> P (S (S n))) -> forall n:nat, P n ).
Print nat_rect.
exact (fun (P : nat -> Type) (f0 : P 0) (f1 : P 1)
  (ff : forall n : nat, P n -> P(S n) -> P (S(S n))) =>
  fix F (n : nat) : P n :=
    match n as n0 return (P n0) with
    | 0 => f0
    | S n' =>  match n' with
       | 0 => f1
       | S n'' => ff n'' (F n'') (F n')
       end
    end).
Qed.

The problem is that F n' has the type (P n') and at that position, but its supposed to be P(S n''). But obviously, S n'' is the same as n' because we are in that case, but Coq cannot detect that. How do I get around with this problem?

Upvotes: 1

Views: 71

Answers (1)

Vinz
Vinz

Reputation: 6057

I would advise to prove the lemma using tactics, are you trying to write the proof term by hand on purpose ?

Anyway, I think that you need to help Coq with the "convoy pattern" so it can unify the two terms. Read more about this technic here.

EDIT proof using tactics: If I recall correctly, there is a "trick" for this proof. You can't prove it directly by induction, because induction goes "one" step at a time, and you need two. The trick is to first prove:

Theorem nat_rect_1_2_gen: forall (P:nat->Type), (P O -> P 1 -> 
  (forall n:nat, P n -> P (S n) -> P (S (S n))) -> forall n:nat, (P n) *(P (S n))).

by induction on n, and then use this result to prove your original goal. The proof will start with:

intros P hP0 hP1 hPS. (* introducing basic assumptions *)
induction n as [ | h [hn hSn]]. (* induction on n *)

and you should be able to figure how to prove each subgoal. If you need more help, I'll give more details.

Upvotes: 2

Related Questions