I want to create a list of mixed types of boolean and nat. This list must hold elements of some super-type: boat where every boolean is a boat and every nat is a boat.
The problem I am having is that this super-type boat should have a boat_eq_dec meaning there should be a way to decide whether two boat's are the same or different. As nat and boolean both have such an equality decider, the super-type should have one as well.
In the example below, I have created a super-type, but I cannot show the equality-deciding lemmaLemma boat_eq_dec : forall x y : Boat, {x = y} + {x <> y}.
Inductive Boat : Set :=
| is_bool (inp: bool)
| is_nat (inp: nat).
What is the correct way to define this super-type, or show the lemma?
You can also directly use (bool + nat)%type (using sum) to get a general notion.
Then decide equality can solve several eq_dec goals.
Definition boat := (bool + nat)%type.
Lemma boat_eq_dec :
forall x y : boat, {x = y} + {x <> y} .
Proof.
intros x y. decide equality.
all: decide equality.
Defined.
You could even consider proving the general lemma
forall A B,
(forall x y : A, {x = y} + {x <> y}) ->
(forall x y : B, {x = y} + {x <> y}) ->
forall x y : A + B, {x = y} + {x <> y}.
It is already proved in the Equations library, but it's probably not worth installing just for this.