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

See Logic and Specif.

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).

I’m learning how to use the FMapInterface class of modules in Coq. A search for FMapInterface led me to A Machine Checked Model of Idempotent MGU Axioms For
Lists of Equational Constraints which had a link to its corresponding Coq script. Poking around in that script led me to the line:

Module Nat_as_MyOT <: UsualOrderedType := Nat_as_OT.

I looked up the meaning of the <: syntax. The reference manual explains that it “starts an interactive module satisfying each” subsequent module type. The ModuleSystemTutorial page also has more information on how modules are used.