Composing sumbools for container type

Question

I'm trying to build an equality predicate returning sumbool instead of bool for a simple type:

Inductive state_type : Set := State : nat -> nat -> state_type.

Here's a working solution, which splits into subgoals based on whether the fields match (one at a time).

Definition state_eq : forall (s1 s2 : state_type), {s1 = s2} + {s1 <> s2}.
  intros.
  destruct s1 as [a1 b1]. destruct s2 as [a2 b2].
  destruct (eq_nat_dec a1 a2) as [Aeq | Aneq]. destruct (eq_nat_dec b1 b2) as [Beq | Bneq].
  left. congruence.
  right. congruence.
  right. congruence.
Defined.

The proof is readable, but I'd like a more direct proof using refine:

Definition state_eq2 : forall (s1 s2 : state_type), {s1 = s2} + {s1 <> s2}.
  refine (fun (s1 s2 : state_type) =>
            match s1, s2 with State a1 b1, State a2 b2 =>
               if (eq_nat_dec a1 a2)
               then if (eq_nat_dec b1 b2)
                    then left _ _
                    else right _ _
               else right _ _
            end).
Defined.

The three return values end up as subgoals, but the context for all of them loses the eq_nat_dec hypotheses, rendering them unprovable. How can I retain these hypotheses to finish the proof?

I don't understand what you mean with "loses the eq_nat_dec hypotheses". For me they show up in the context. See here: x80.org/collacoq/paqejibosi.coq . What version of Coq are you using? — larsr
Hmm you're right. Not sure what I was doing differently since I now I can't reproduce either — Felipe

Felipe Felipe · Accepted Answer · 2021-06-17T18:13:21

It seems that if ... then ... else is what's losing those hypotheses. Replacing it with an explicit match preserves the hypotheses, allowing congruence to finish off the proof as before:

Definition state_eq : forall (s1 s2 : state_type), {s1 = s2} + {s1 <> s2}.
  refine (fun (s1 s2 : state_type) =>
            match s1, s2 with State a1 b1, State a2 b2 =>
               match (eq_nat_dec a1 a2) with
                 | left _ => match (eq_nat_dec b1 b2) with
                               | left _ => left _ _
                               | right _ => right _ _
                             end
                 | right _ => right _ _
               end
            end); congruence.
Defined.

Composing sumbools for container type

1 Answers