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.