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.

While working on the Lists section of Software Foundations, I tried to define member as follows:

Definition member (v:nat) (s:bag) : bool :=
match gt (count v s) 0 with
| False => false
| True => true
end.

I kept getting “Error: This clause is redundant.” After some digging around, I found Adam’s explanation that logical propositions (Prop) such as gt (count v s) 0 are not usable for pattern matching in Gallina (without solving “the halting problem and more”). The easier solution then hit me (duh):

Definition member (v:nat) (s:bag) : bool :=
match count v s with
| O => false
| _ => true
end.

Thankfully, I learned something new about Prop though :).

The difference between Require Import MyModule and Require Export MyModule is well explained in the modules tutorial:

If a required module depends on other modules then the latter’s are automatically required beforehand. However their contents are not automatically visible. If you want a module M required in a module N to be automatically visible when N is required, you should use Require Export M in your module N.