How do I reason about conditionals in Coq?
-
16-02-2021 - |
Question
I'm working through the ListSet
module from the Coq standard library. I'm unsure how to reason about conditionals in a proof. For instance, I am having trouble with the following proof. Definitions are provided for context.
Fixpoint set_mem (x : A) (xs : set) : bool :=
match xs with
| nil => false
| cons y ys =>
match Aeq_dec x y with
| left _ => true
| right _ => set_mem x ys
end
end.
Definition set_In : A -> set -> Prop := In (A := A).
Lemma set_mem_correct1 : forall (x : A) (xs : set),
set_mem x xs = true -> set_In x xs.
Proof. intros. induction xs.
discriminate.
simpl; destruct Aeq_dec with a x.
intuition.
simpl in H.
The current proof state includes the inr
of Aeq_dec
as a hypothesis. I have discarded the base case of induction and the inductive case where the inl
of Aeq_dec
is true.
A : Type
Aeq_dec : forall x y : A, {x = y} + {x <> y}
x : A
a : A
xs : list A
H : (if Aeq_dec x a then true else set_mem x xs) = true
IHxs : set_mem x xs = true -> set_In x xs
n : a <> x
============================
a = x \/ set_In x xs
The only way for H
to be true if a <> x
is if set_mem xs
is true. I should be able to apply the conditional in H
to a <> x
in order to obtain set_mem xs
. However, I don't understand how to do this. How do I deal with, or decompose, or apply conditionals?
Solution
Have you tried this? (syntax may be buggy, no coqtop here atm)
destruct (Aeq_dec x a);
[ subst; elim (n eq_refl)
| right; apply (IHxs H)
].
(if <foo>
is more or less the same as match <foo> with
. You'll have to reduce (destruct
, case
, ...) such that the match can be decided (or for the if
, things must reduce to either the first or the second constructor of whatever type you're using it with.) Most of the time, you'll need the value that gets case-analyzed (though not here). If you need it, do a remember (<value>) as foo; destruct foo
instead of destructing directly.)