diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/dependentind.v | 46 |
1 files changed, 27 insertions, 19 deletions
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v index 4825538691..48b07db83d 100644 --- a/test-suite/success/dependentind.v +++ b/test-suite/success/dependentind.v @@ -1,10 +1,10 @@ Require Import Coq.Program.Program. -Set Implicit Arguments. -Unset Strict Implicit. +Set Manual Implicit Arguments. + Variable A : Set. -Inductive vector : nat -> Type := vnil : vector 0 | vcons : A -> forall n, vector n -> vector (S n). +Inductive vector : nat -> Type := vnil : vector 0 | vcons : A -> forall {n}, vector n -> vector (S n). Goal forall n, forall v : vector (S n), vector n. Proof. @@ -35,24 +35,32 @@ Inductive ctx : Type := | empty : ctx | snoc : ctx -> type -> ctx. -Notation " Γ , τ " := (snoc Γ τ) (at level 25, t at next level, left associativity). +Bind Scope context_scope with ctx. +Delimit Scope context_scope with ctx. + +Arguments Scope snoc [context_scope]. + +Notation " Γ , τ " := (snoc Γ τ) (at level 25, t at next level, left associativity) : context_scope. -Fixpoint conc (Γ Δ : ctx) : ctx := +Fixpoint conc (Δ Γ : ctx) : ctx := match Δ with | empty => Γ - | snoc Δ' x => snoc (conc Γ Δ') x + | snoc Δ' x => snoc (conc Δ' Γ) x end. -Notation " Γ ; Δ " := (conc Γ Δ) (at level 25, left associativity). +Notation " Γ ;; Δ " := (conc Δ Γ) (at level 25, left associativity) : context_scope. Inductive term : ctx -> type -> Type := -| ax : forall Γ τ, term (Γ, τ) τ -| weak : forall Γ τ, term Γ τ -> forall τ', term (Γ, τ') τ -| abs : forall Γ τ τ', term (Γ , τ) τ' -> term Γ (τ --> τ') +| ax : forall Γ τ, term (snoc Γ τ) τ +| weak : forall Γ τ, term Γ τ -> forall τ', term (snoc Γ τ') τ +| abs : forall Γ τ τ', term (snoc Γ τ) τ' -> term Γ (τ --> τ') | app : forall Γ τ τ', term Γ (τ --> τ') -> term Γ τ -> term Γ τ'. -Lemma weakening : forall Γ Δ τ, term (Γ ; Δ) τ -> - forall τ', term (Γ , τ' ; Δ) τ. +Notation " Γ |- τ " := (term Γ τ) (at level 0). + + +Lemma weakening : forall Γ Δ τ, term (Γ ;; Δ) τ -> + forall τ', term (Γ , τ' ;; Δ) τ. Proof with simpl in * ; auto ; simpl_depind. intros Γ Δ τ H. @@ -64,21 +72,21 @@ Proof with simpl in * ; auto ; simpl_depind. apply ax. destruct Δ... - specialize (IHterm Γ empty)... - apply weak... + specialize (IHterm empty Γ)... + apply weak... apply weak... destruct Δ... - apply weak ; apply abs ; apply H. + apply weak. apply abs ; apply H. apply abs... - specialize (IHterm Γ0 (Δ, t, τ))... + specialize (IHterm (Δ, t, τ)%ctx Γ0)... apply app with τ... Qed. -Lemma exchange : forall Γ Δ α β τ, term (Γ, α, β ; Δ) τ -> term (Γ, β, α ; Δ) τ. +Lemma exchange : forall Γ Δ α β τ, term (Γ, α, β ;; Δ) τ -> term (Γ, β, α ;; Δ) τ. Proof with simpl in * ; simpl_depind ; auto. intros until 1. dependent induction H. @@ -89,12 +97,12 @@ Proof with simpl in * ; simpl_depind ; auto. apply ax. destruct Δ... - pose (weakening (Γ:=Γ0) (Δ:=(empty, α)))... + pose (weakening Γ0 (empty, α))... apply weak... apply abs... - specialize (IHterm Γ0 α β (Δ, τ))... + specialize (IHterm (Δ, τ)%ctx Γ0 α β)... eapply app with τ... Save. |