1 files changed, 85 insertions, 0 deletions
diff --git a/contrib7/ring/Quote.v b/contrib7/ring/Quote.v
new file mode 100644
index 00000000..12a51c9f
--- /dev/null
+++ b/contrib7/ring/Quote.v
@@ -0,0 +1,85 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: Quote.v,v 1.1.2.1 2004/07/16 19:30:18 herbelin Exp $ *)
+
+(***********************************************************************
+  The "abstract" type index is defined to represent variables.
+
+  index : Set
+  index_eq : index -> bool
+  index_eq_prop: (n,m:index)(index_eq n m)=true -> n=m
+  index_lt : index -> bool
+  varmap : Type -> Type.	
+  varmap_find : (A:Type)A -> index -> (varmap A) -> A.
+
+  The first arg. of varmap_find is the default value to take
+  if the object is not found in the varmap.
+
+  index_lt defines a total well-founded order, but we don't prove that.
+
+***********************************************************************)
+
+Set Implicit Arguments.
+
+Section variables_map.
+
+Variable A : Type.
+
+Inductive varmap : Type :=
+  Empty_vm : varmap
+| Node_vm : A->varmap->varmap->varmap.
+
+Inductive index : Set := 
+| Left_idx : index -> index
+| Right_idx : index -> index
+| End_idx : index
+.
+
+Fixpoint varmap_find [default_value:A; i:index; v:varmap] : A :=
+  Cases i v of
+    End_idx (Node_vm x _ _) => x
+  | (Right_idx i1) (Node_vm x v1 v2) => (varmap_find default_value i1 v2)
+  | (Left_idx i1) (Node_vm x v1 v2) => (varmap_find default_value i1 v1)
+  | _ _ => default_value
+  end.
+
+Fixpoint index_eq [n,m:index] : bool :=
+  Cases n m of
+  | End_idx End_idx => true
+  | (Left_idx n') (Left_idx m') => (index_eq n' m')
+  | (Right_idx n') (Right_idx m') => (index_eq n' m')
+  | _ _ => false
+  end.
+
+Fixpoint index_lt[n,m:index] : bool :=
+  Cases n m of
+  | End_idx (Left_idx _) => true
+  | End_idx (Right_idx _) => true
+  | (Left_idx n') (Right_idx m') => true
+  | (Right_idx n') (Right_idx m') => (index_lt n' m') 
+  | (Left_idx n') (Left_idx m') => (index_lt n' m') 
+  | _ _ => false
+  end.
+
+Lemma index_eq_prop : (n,m:index)(index_eq n m)=true -> n=m.
+  Induction n; Induction m; Simpl; Intros.
+  Rewrite (H i0 H1); Reflexivity.
+  Discriminate.
+  Discriminate.
+  Discriminate.
+  Rewrite (H i0 H1); Reflexivity.
+  Discriminate.
+  Discriminate.
+  Discriminate.
+  Reflexivity.
+Save.
+
+End variables_map.
+
+Unset Implicit Arguments.