summaryrefslogtreecommitdiff
path: root/test-suite/success/conv_pbs.v
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
committerGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
commita0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
treedabcac548e299fee1da464c93b3dba98484f45b1 /test-suite/success/conv_pbs.v
parent2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'test-suite/success/conv_pbs.v')
-rw-r--r--test-suite/success/conv_pbs.v223
1 files changed, 223 insertions, 0 deletions
diff --git a/test-suite/success/conv_pbs.v b/test-suite/success/conv_pbs.v
new file mode 100644
index 00000000..062c3ee5
--- /dev/null
+++ b/test-suite/success/conv_pbs.v
@@ -0,0 +1,223 @@
+(* A bit complex but realistic example whose last fixpoint definition
+ used to fail in 8.1 because of wrong environment in conversion
+ problems (see revision 9664) *)
+
+Require Import List.
+Require Import Arith.
+
+Parameter predicate : Set.
+Parameter function : Set.
+Definition variable := nat.
+Definition x0 := 0.
+Definition var_eq_dec := eq_nat_dec.
+
+Inductive term : Set :=
+ | App : function -> term -> term
+ | Var : variable -> term.
+
+Definition atom := (predicate * term)%type.
+
+Inductive formula : Set :=
+ | Atom : atom -> formula
+ | Imply : formula -> formula -> formula
+ | Forall : variable -> formula -> formula.
+
+Notation "A --> B" := (Imply A B) (at level 40).
+
+Definition substitution range := list (variable * range).
+
+Fixpoint remove_assoc (A:Set)(x:variable)(rho: substitution A){struct rho}
+ : substitution A :=
+ match rho with
+ | nil => rho
+ | (y,t) :: rho => if var_eq_dec x y then remove_assoc A x rho
+ else (y,t) :: remove_assoc A x rho
+ end.
+
+Fixpoint assoc (A:Set)(x:variable)(rho:substitution A){struct rho}
+ : option A :=
+ match rho with
+ | nil => None
+ | (y,t) :: rho => if var_eq_dec x y then Some t
+ else assoc A x rho
+ end.
+
+Fixpoint subst_term (rho:substitution term)(t:term){struct t} : term :=
+ match t with
+ | Var x => match assoc _ x rho with
+ | Some a => a
+ | None => Var x
+ end
+ | App f t' => App f (subst_term rho t')
+ end.
+
+Fixpoint subst_formula (rho:substitution term)(A:formula){struct A}:formula :=
+ match A with
+ | Atom (p,t) => Atom (p, subst_term rho t)
+ | A --> B => subst_formula rho A --> subst_formula rho B
+ | Forall y A => Forall y (subst_formula (remove_assoc _ y rho) A)
+ (* assume t closed *)
+ end.
+
+Definition subst A x t := subst_formula ((x,t):: nil) A.
+
+Record Kripke : Type := {
+ worlds: Set;
+ wle : worlds -> worlds -> Type;
+ wle_refl : forall w, wle w w ;
+ wle_trans : forall w w' w'', wle w w' -> wle w' w'' -> wle w w'';
+ domain : Set;
+ vars : variable -> domain;
+ funs : function -> domain -> domain;
+ atoms : worlds -> predicate * domain -> Type;
+ atoms_mon : forall w w', wle w w' -> forall P, atoms w P -> atoms w' P
+}.
+
+Section Sem.
+
+Variable K : Kripke.
+
+Fixpoint sem (rho: substitution (domain K))(t:term){struct t} : domain K :=
+ match t with
+ | Var x => match assoc _ x rho with
+ | Some a => a
+ | None => vars K x
+ end
+ | App f t' => funs K f (sem rho t')
+ end.
+
+End Sem.
+
+Notation "w <= w'" := (wle _ w w').
+
+Set Implicit Arguments.
+
+Reserved Notation "w ||- A" (at level 70).
+
+Definition context := list formula.
+
+Variable fresh : variable -> context -> Prop.
+
+Variable fresh_out : context -> variable.
+
+Axiom fresh_out_spec : forall Gamma, fresh (fresh_out Gamma) Gamma.
+
+Axiom fresh_peel : forall x A Gamma, fresh x (A::Gamma) -> fresh x Gamma.
+
+Fixpoint force (K:Kripke)(rho: substitution (domain K))(w:worlds K)(A:formula)
+ {struct A} : Type :=
+ match A with
+ | Atom (p,t) => atoms K w (p, sem K rho t)
+ | A --> B => forall w', w <= w' -> force K rho w' A -> force K rho w' B
+ | Forall x A => forall w', w <= w' -> forall t, force K ((x,t)::remove_assoc _ x rho) w' A
+ end.
+
+Notation "w ||- A" := (force _ nil w A).
+
+Reserved Notation "Gamma |- A" (at level 70).
+Reserved Notation "Gamma ; A |- C" (at level 70, A at next level).
+
+Inductive context_prefix (Gamma:context) : context -> Type :=
+ | CtxPrefixRefl : context_prefix Gamma Gamma
+ | CtxPrefixTrans : forall A Gamma', context_prefix Gamma Gamma' -> context_prefix Gamma (cons A Gamma').
+
+Inductive in_context (A:formula) : list formula -> Prop :=
+ | InAxiom : forall Gamma, in_context A (cons A Gamma)
+ | OmWeak : forall Gamma B, in_context A Gamma -> in_context A (cons B Gamma).
+
+Inductive prove : list formula -> formula -> Type :=
+ | ProofImplyR : forall A B Gamma, prove (cons A Gamma) B
+ -> prove Gamma (A --> B)
+ | ProofForallR : forall x A Gamma, (forall y, fresh y (A::Gamma)
+ -> prove Gamma (subst A x (Var y))) -> prove Gamma (Forall x A)
+ | ProofCont : forall A Gamma Gamma' C, context_prefix (A::Gamma) Gamma'
+ -> (prove_stoup Gamma' A C) -> (Gamma' |- C)
+
+where "Gamma |- A" := (prove Gamma A)
+
+ with prove_stoup : list formula -> formula -> formula -> Type :=
+ | ProofAxiom Gamma C: Gamma ; C |- C
+ | ProofImplyL Gamma C : forall A B, (Gamma |- A)
+ -> (prove_stoup Gamma B C) -> (prove_stoup Gamma (A --> B) C)
+ | ProofForallL Gamma C : forall x t A, (prove_stoup Gamma (subst A x t) C)
+ -> (prove_stoup Gamma (Forall x A) C)
+
+where " Gamma ; B |- A " := (prove_stoup Gamma B A).
+
+Axiom context_prefix_trans :
+ forall Gamma Gamma' Gamma'',
+ context_prefix Gamma Gamma'
+ -> context_prefix Gamma' Gamma''
+ -> context_prefix Gamma Gamma''.
+
+Axiom Weakening :
+ forall Gamma Gamma' A,
+ context_prefix Gamma Gamma' -> Gamma |- A -> Gamma' |- A.
+
+Axiom universal_weakening :
+ forall Gamma Gamma', context_prefix Gamma Gamma'
+ -> forall P, Gamma |- Atom P -> Gamma' |- Atom P.
+
+Canonical Structure Universal := Build_Kripke
+ context
+ context_prefix
+ CtxPrefixRefl
+ context_prefix_trans
+ term
+ Var
+ App
+ (fun Gamma P => Gamma |- Atom P)
+ universal_weakening.
+
+Axiom subst_commute :
+ forall A rho x t,
+ subst_formula ((x,t)::rho) A = subst (subst_formula rho A) x t.
+
+Axiom subst_formula_atom :
+ forall rho p t,
+ Atom (p, sem _ rho t) = subst_formula rho (Atom (p,t)).
+
+Fixpoint universal_completeness (Gamma:context)(A:formula){struct A}
+ : forall rho:substitution term,
+ force _ rho Gamma A -> Gamma |- subst_formula rho A
+ :=
+ match A
+ return forall rho, force _ rho Gamma A
+ -> Gamma |- subst_formula rho A
+ with
+ | Atom (p,t) => fun rho H => eq_rect _ (fun A => Gamma |- A) H _ (subst_formula_atom rho p t)
+ | A --> B => fun rho HImplyAB =>
+ let A' := subst_formula rho A in
+ ProofImplyR (universal_completeness (A'::Gamma) B rho
+ (HImplyAB (A'::Gamma)(CtxPrefixTrans A' (CtxPrefixRefl Gamma))
+ (universal_completeness_stoup A rho (fun C Gamma' Hle p
+ => ProofCont Hle p))))
+ | Forall x A => fun rho HForallA
+ => ProofForallR x (fun y Hfresh
+ => eq_rect _ _ (universal_completeness Gamma A _
+ (HForallA Gamma (CtxPrefixRefl Gamma)(Var y))) _ (subst_commute _ _ _ _ ))
+ end
+with universal_completeness_stoup (Gamma:context)(A:formula){struct A}
+ : forall rho, (forall C Gamma', context_prefix Gamma Gamma'
+ -> Gamma' ; subst_formula rho A |- C -> Gamma' |- C)
+ -> force _ rho Gamma A
+ :=
+ match A return forall rho,
+ (forall C Gamma', context_prefix Gamma Gamma'
+ -> Gamma' ; subst_formula rho A |- C
+ -> Gamma' |- C)
+ -> force _ rho Gamma A
+ with
+ | Atom (p,t) as C => fun rho H
+ => H _ Gamma (CtxPrefixRefl Gamma)(ProofAxiom _ _)
+ | A --> B => fun rho H => fun Gamma' Hle HA
+ => universal_completeness_stoup B rho (fun C Gamma'' Hle' p
+ => H C Gamma'' (context_prefix_trans Hle Hle')
+ (ProofImplyL (Weakening Hle' (universal_completeness Gamma' A rho HA)) p))
+ | Forall x A => fun rho H => fun Gamma' Hle t
+ => (universal_completeness_stoup A ((x,t)::remove_assoc _ x rho)
+ (fun C Gamma'' Hle' p =>
+ H C Gamma'' (context_prefix_trans Hle Hle')
+ (ProofForallL x t (subst_formula (remove_assoc _ x rho) A)
+ (eq_rect _ (fun D => Gamma'' ; D |- C) p _ (subst_commute _ _ _ _)))))
+ end.