1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
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.
|
