diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-16 14:50:35 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-16 14:50:35 +0000 |
| commit | a4deb2c27bdbbba5053c0b25a326ee24a2f42e1a (patch) | |
| tree | 29c8c169e287fdffd89a2f88d5628230ca8c952f /test-suite/success/dependentind.v | |
| parent | a76ad2ccdc57f54bd23e1c64f3f4a4af8e912050 (diff) | |
Misc: Add test for bug 1704, now closed. Add usual syntax for lists in
Program.Syntax along with stronger implicits. Update dependent induction
test file using unicode syntax.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10682 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/dependentind.v')
| -rw-r--r-- | test-suite/success/dependentind.v | 59 |
1 files changed, 28 insertions, 31 deletions
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v index 77bc295fd..8b8ce0098 100644 --- a/test-suite/success/dependentind.v +++ b/test-suite/success/dependentind.v @@ -35,69 +35,66 @@ Inductive ctx : Type := | empty : ctx | snoc : ctx -> type -> ctx. -Notation " G , tau " := (snoc G tau) (at level 20, t at next level). +Notation " Γ , τ " := (snoc Γ τ) (at level 20, t at next level). -Fixpoint conc (G D : ctx) : ctx := - match D with - | empty => G - | snoc D' x => snoc (conc G D') x +Fixpoint conc (Γ Δ : ctx) : ctx := + match Δ with + | empty => Γ + | snoc Δ' x => snoc (conc Γ Δ') x end. -Notation " G ; D " := (conc G D) (at level 20). +Notation " Γ ; Δ " := (conc Γ Δ) (at level 20). Inductive term : ctx -> type -> Type := -| ax : forall G tau, term (G, tau) tau -| weak : forall G tau, - term G tau -> forall tau', term (G, tau') tau -| abs : forall G tau tau', - term (G , tau) tau' -> term G (tau --> tau') -| app : forall G tau tau', - term G (tau --> tau') -> term G tau -> term G tau'. - -Lemma weakening : forall G D tau, term (G ; D) tau -> - forall tau', term (G , tau' ; D) tau. +| ax : forall Γ τ, term (Γ, τ) τ +| weak : forall Γ τ, term Γ τ -> forall τ', term (Γ, τ') τ +| abs : forall Γ τ τ', term (Γ , τ) τ' -> term Γ (τ --> τ') +| app : forall Γ τ τ', term Γ (τ --> τ') -> term Γ τ -> term Γ τ'. + +Lemma weakening : forall Γ Δ τ, term (Γ ; Δ) τ -> + forall τ', term (Γ , τ' ; Δ) τ. Proof with simpl in * ; auto ; simpl_depind. - intros G D tau H. + intros Γ Δ τ H. - dependent induction H generalizing G D. + dependent induction H generalizing Γ Δ. - destruct D... + destruct Δ... apply weak ; apply ax. apply ax. - destruct D... - specialize (IHterm G empty)... + destruct Δ... + specialize (IHterm Γ empty)... apply weak... apply weak... - destruct D... + destruct Δ... apply weak ; apply abs ; apply H. apply abs... - specialize (IHterm G0 (D, t, tau))... + specialize (IHterm Γ0 (Δ, t, τ))... - apply app with tau... + apply app with τ... Qed. -Lemma exchange : forall G D alpha bet tau, term (G, alpha, bet ; D) tau -> term (G, bet, alpha ; D) tau. +Lemma exchange : forall Γ Δ α β τ, term (Γ, α, β ; Δ) τ -> term (Γ, β, α ; Δ) τ. Proof with simpl in * ; simpl_depind ; auto. intros until 1. - dependent induction H generalizing G D alpha bet... + dependent induction H generalizing Γ Δ α β... - destruct D... + destruct Δ... apply weak ; apply ax. apply ax. - destruct D... - pose (weakening (G:=G0) (D:=(empty, alpha)))... + destruct Δ... + pose (weakening (Γ:=Γ0) (Δ:=(empty, α)))... apply weak... apply abs... - specialize (IHterm G0 (D, tau))... + specialize (IHterm Γ0 (Δ, τ))... - eapply app with tau... + eapply app with τ... Save. |