diff options
Diffstat (limited to 'test-suite/success/dependentind.v')
| -rw-r--r-- | test-suite/success/dependentind.v | 87 |
1 files changed, 58 insertions, 29 deletions
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v index 48255386..488b057f 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,51 +35,55 @@ 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). -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 (Γ ,, τ') τ +| abs : forall Γ τ τ', term (snoc Γ τ) τ' -> term Γ (τ --> τ') | app : forall Γ τ τ', term Γ (τ --> τ') -> term Γ τ -> term Γ τ'. -Lemma weakening : forall Γ Δ τ, term (Γ ; Δ) τ -> - forall τ', term (Γ , τ' ; Δ) τ. -Proof with simpl in * ; auto ; simpl_depind. +Hint Constructors term : lambda. + +Open Local Scope context_scope. + +Notation " Γ |-- τ " := (term Γ τ) (at level 0) : type_scope. + +Lemma weakening : forall Γ Δ τ, term (Γ ;; Δ) τ -> + forall τ', term (Γ ,, τ' ;; Δ) τ. +Proof with simpl in * ; reverse ; simplify_dep_elim ; simplify_IH_hyps ; eauto with lambda. intros Γ Δ τ H. dependent induction H. destruct Δ... - apply weak ; apply ax. - - apply ax. - - destruct Δ... - specialize (IHterm Γ empty)... - apply weak... - - apply weak... destruct Δ... - apply weak ; apply abs ; apply H. + destruct Δ... apply abs... - specialize (IHterm Γ0 (Δ, t, τ))... + + specialize (IHterm (Δ,, t,, τ)%ctx Γ0)... + intro. apply app with τ... Qed. -Lemma exchange : forall Γ Δ α β τ, term (Γ, α, β ; Δ) τ -> term (Γ, β, α ; Δ) τ. -Proof with simpl in * ; simpl_depind ; auto. +Lemma exchange : forall Γ Δ α β τ, term (Γ,, α,, β ;; Δ) τ -> term (Γ,, β,, α ;; Δ) τ. +Proof with simpl in * ; subst ; reverse ; simplify_dep_elim ; simplify_IH_hyps ; auto. intros until 1. dependent induction H. @@ -89,12 +93,37 @@ 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 α β (Δ, τ))... + apply abs... + specialize (IHterm (Δ ,, τ))... eapply app with τ... Save. + +(** Example by Andrew Kenedy, uses simplification of the first component of dependent pairs. *) + +Unset Manual Implicit Arguments. + +Inductive Ty := + | Nat : Ty + | Prod : Ty -> Ty -> Ty. + +Inductive Exp : Ty -> Type := +| Const : nat -> Exp Nat +| Pair : forall t1 t2, Exp t1 -> Exp t2 -> Exp (Prod t1 t2) +| Fst : forall t1 t2, Exp (Prod t1 t2) -> Exp t1. + +Inductive Ev : forall t, Exp t -> Exp t -> Prop := +| EvConst : forall n, Ev (Const n) (Const n) +| EvPair : forall t1 t2 (e1:Exp t1) (e2:Exp t2) e1' e2', + Ev e1 e1' -> Ev e2 e2' -> Ev (Pair e1 e2) (Pair e1' e2') +| EvFst : forall t1 t2 (e:Exp (Prod t1 t2)) e1 e2, + Ev e (Pair e1 e2) -> + Ev (Fst e) e1. + +Lemma EvFst_inversion : forall t1 t2 (e:Exp (Prod t1 t2)) e1, Ev (Fst e) e1 -> exists e2, Ev e (Pair e1 e2). +intros t1 t2 e e1 ev. dependent destruction ev. exists e2 ; assumption. +Qed. |