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?

Answer 1

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

友情链接