Library Coq.quote.Quote
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) {
struct v} :
A :=
match i,
v with
|
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) {
struct m} :
bool :=
match n,
m with
|
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) {
struct m} :
bool :=
match n,
m with
|
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 :
forall n m:
index,
index_eq n m = true -> n = m.
End variables_map.
Unset Implicit Arguments.