diff options
author | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-02-04 17:37:07 +0000 |
---|---|---|
committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-02-04 17:37:07 +0000 |
commit | 14e4261beb81ba792dc1e42ddf52f24c04596150 (patch) | |
tree | 3f30e419e90092535bfd6202d492d152f7aaa891 /test-suite/success/dependentind.v | |
parent | 46efe4d675bb96704cf9c598f456a2999b013dbc (diff) |
Report r11631 from 8.2 and handle non-dependent goals better in
[dependent induction].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11881 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/dependentind.v')
-rw-r--r-- | test-suite/success/dependentind.v | 54 |
1 files changed, 29 insertions, 25 deletions
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v index 488b057f3..3ab7682d9 100644 --- a/test-suite/success/dependentind.v +++ b/test-suite/success/dependentind.v @@ -40,7 +40,7 @@ Delimit Scope context_scope with ctx. Arguments Scope snoc [context_scope]. -Notation " Γ ,, τ " := (snoc Γ τ) (at level 25, t at next level, left associativity). +Notation " Γ , τ " := (snoc Γ τ) (at level 25, τ at next level, left associativity) : context_scope. Fixpoint conc (Δ Γ : ctx) : ctx := match Δ with @@ -48,60 +48,64 @@ Fixpoint conc (Δ Γ : ctx) : ctx := | snoc Δ' x => snoc (conc Δ' Γ) x end. -Notation " Γ ;; Δ " := (conc Δ Γ) (at level 25, left associativity) : context_scope. +Notation " Γ ; Δ " := (conc Δ Γ) (at level 25, left associativity) : context_scope. + +Reserved Notation " Γ ⊢ τ " (at level 30, no associativity). Inductive term : ctx -> type -> Type := -| ax : forall Γ τ, term (snoc Γ τ) τ -| weak : forall Γ τ, term Γ τ -> forall τ', term (Γ ,, τ') τ -| abs : forall Γ τ τ', term (snoc Γ τ) τ' -> term Γ (τ --> τ') -| app : forall Γ τ τ', term Γ (τ --> τ') -> term Γ τ -> term Γ τ'. +| ax : `(Γ, τ ⊢ τ) +| weak : `{Γ ⊢ τ -> Γ, τ' ⊢ τ} +| abs : `{Γ, τ ⊢ τ' -> Γ ⊢ τ --> τ'} +| app : `{Γ ⊢ τ --> τ' -> Γ ⊢ τ -> Γ ⊢ τ'} + +where " Γ ⊢ τ " := (term Γ τ) : type_scope. Hint Constructors term : lambda. Open Local Scope context_scope. -Notation " Γ |-- τ " := (term Γ τ) (at level 0) : type_scope. +Ltac eqns := subst ; reverse ; simplify_dep_elim ; simplify_IH_hyps. -Lemma weakening : forall Γ Δ τ, term (Γ ;; Δ) τ -> - forall τ', term (Γ ,, τ' ;; Δ) τ. -Proof with simpl in * ; reverse ; simplify_dep_elim ; simplify_IH_hyps ; eauto with lambda. +Lemma weakening : forall Γ Δ τ, Γ ; Δ ⊢ τ -> + forall τ', Γ , τ' ; Δ ⊢ τ. +Proof with simpl in * ; eqns ; eauto with lambda. intros Γ Δ τ H. dependent induction H. - destruct Δ... + destruct Δ as [|Δ τ']... - destruct Δ... + destruct Δ as [|Δ τ'']... - destruct Δ... - apply abs... - - specialize (IHterm (Δ,, t,, τ)%ctx Γ0)... + destruct Δ as [|Δ τ'']... + apply abs. - intro. - apply app with τ... + specialize (IHterm (Δ, τ'', τ) Γ0)... + + intro. eapply app... Qed. -Lemma exchange : forall Γ Δ α β τ, term (Γ,, α,, β ;; Δ) τ -> term (Γ,, β,, α ;; Δ) τ. -Proof with simpl in * ; subst ; reverse ; simplify_dep_elim ; simplify_IH_hyps ; auto. +Lemma exchange : forall Γ Δ α β τ, term (Γ, α, β ; Δ) τ -> term (Γ, β, α ; Δ) τ. +Proof with simpl in * ; eqns ; eauto. intros until 1. + dependent induction H. - destruct Δ... + destruct Δ ; eqns. apply weak ; apply ax. apply ax. destruct Δ... - pose (weakening Γ0 (empty,, α))... + pose (weakening Γ0 (empty, α))... apply weak... apply abs... - specialize (IHterm (Δ ,, τ))... + specialize (IHterm (Δ, τ))... - eapply app with τ... -Save. + eapply app... +Defined. (** Example by Andrew Kenedy, uses simplification of the first component of dependent pairs. *) |