Skip to Content.
Sympa Menu

coq-club - [Coq-Club] help with dependent induction

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] help with dependent induction


chronological Thread 
  • From: Andrew Polonsky <andrew.polonsky AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] help with dependent induction
  • Date: Tue, 21 Feb 2012 21:00:03 +0100
  • Authentication-results: mr.google.com; spf=pass (google.com: domain of andrew.polonsky AT gmail.com designates 10.229.78.89 as permitted sender) smtp.mail=andrew.polonsky AT gmail.com; dkim=pass header.i=andrew.polonsky AT gmail.com

Hello,

I'm having trouble proving a simple goal about the following type,
representing 1-step call-by-name reduction of lambda terms with
deBruijn levels:

Inductive wred {d:nat} : @Lambda d -> @Lambda d -> Set :=
| wred_here (re : @Lambda (S d)) (dex : Lambda)
    : wred (app (abs re) dex) (root_red re dex)
| wred_left (s s' t : Lambda) : wred s s' -> wred (app s t) (app s' t).

The goal states that there is at most one contraction of s to t:

Lemma wred_inj2 {d:nat} (s t: @Lambda d) (wst: wred s t)
                : forall wst': wred s t, wst = wst'.

the following steps get me some of the way,

destruct s.
inversion wst.
Focus 2. inversion wst.
generalize wst.
clear wst.
generalize s1.
dependent inversion_clear wst.
generalize re s2.
clear.

but when I try
dependent inversion wst'.
it gives the error "abstracting over ... is ill-typed".

I understand that the "dependent induction" tactic could be of help,
but I would like to avoid additional axioms if possible, and also to
understand the actual proof.

Thanks in advance!
Andrew


Require Import Arith.

Inductive Lambda {d:nat} : Set :=
  var (i:nat) : (i<d) -> Lambda
| app (s t: Lambda) : Lambda
| abs (r : @Lambda (S d)) : Lambda.

Fixpoint dig {n:nat} (M:Lambda) := match M with
  var i l => var i (lt_S i n l)
| app s t => app (dig s) (dig t)
| abs r   => abs (dig r)
end.

Fixpoint subst {n:nat} (M: @Lambda (S n)) (N: @Lambda n) (k:nat) (l: k <= n)
         : @Lambda n.
refine (match M with
  var i li => _
| app s t => app (subst n s N k l) (subst n t N k l)
| abs r => abs (subst (S n) r (dig N) k (le_S k n l))
end).
case_eq (nat_compare i k).
intro H1; exact N.
intro H2; exact (var i (lt_le_trans i k n (nat_compare_Lt_lt i k H2) l)).
intro H3; rewrite (S_pred i k (nat_compare_Gt_gt i k H3)) in li.
exact (var (pred i) (lt_S_n (pred i) n li)).
Defined.

Definition root_red {d:nat} (re dex: Lambda) := subst re dex O (le_O_n d).

Inductive wred {d:nat} : @Lambda d -> @Lambda d -> Set :=
| wred_here (re : @Lambda (S d)) (dex : Lambda)
    : wred (app (abs re) dex) (root_red re dex)
| wred_left (s s' t : Lambda) : wred s s' -> wred (app s t) (app s' t).

Lemma wred_inj2 {d:nat} (s t: @Lambda d) (wst: wred s t)
                : forall wst': wred s t, wst = wst'.
Proof.
destruct s.
inversion wst.
Focus 2. inversion wst.
generalize wst.
clear wst.
generalize s1.
dependent inversion_clear wst.
generalize re s2.
clear.



Archive powered by MhonArc 2.6.16.

Top of Page