The difference between {x = y} + {x <> y} and x \/ y is whether the result is of type Prop or type Set.
Inductive or (A B:Prop) : Prop :=
| or_introl : A -> A \/ B
| or_intror : B -> A \/ B
The only feature of Section is to apply all the “Variable”s as implicit first arguments to everything listed in the particular section.
Searching for an element in a list is essentially an existsb operation.
Compare the following theorems:
Theorem C_eq_dec:
forall (x y:C), {x = y} + {x <> y}.
Proof.
intros x y.
decide equality.
apply id_eq_dec.
Qed.
Theorem C_eq_dec:
forall (x y:C), {x = y} + {x <> y}.
Proof.
intros x; case x as [|id_x]; intros y; case y as [|id_y]; eauto.
right; intros H; inversion H.
right; intros H; inversion H.
case (id_eq_dec id_x id_y) as [EQ|NEQ]; [ rewrite EQ; left | right ]; eauto.
intros H; eapply NEQ; inversion H; eauto.
Qed.
The first version uses the decide equality tactic. Note that the ML program can be obtained using “Extraction C_eq_dec.” C_eq_dec is also a function that can now be called. For example, it can appear in a match expression like:
match C_eq_dec c c’ with
| right _ => None
| left _ => Some (HeapObj c cfll)
end
where left and right constructors are explained in Specif (under Inductive sumbool …).
As for declaring “Heap” as a map, here is the syntax I finally got to work. Apparently the requires are important (using fully qualified names without them did not work).
Require Import Coq.FSets.FMapWeakList.
Require Import OrderedTypeEx.
Module MyModule (Heap:FMapInterface.S with Module E := Nat_as_OT).