3

ListSetCoq標準ライブラリのモジュールを使用しています。証明の条件について推論する方法がわかりません。たとえば、次の証明に問題があります。コンテキストの定義が提供されています。

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.

現在の証明状態にはinr、Aeq_dec仮説としてのが含まれています。inl帰納の基本ケースとのAeq_decが真である帰納ケースを破棄しました。

  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

真であるための唯一の方法はH、真であるa <> x場合set_mem xsです。を取得するためにH、に条件を適用できるはずです。しかし、私はこれを行う方法を理解していません。条件を処理、分解、または適用するにはどうすればよいですか？a <> xset_mem xs

4

1 に答える 1

2

これを試しましたか？（構文はバグがある可能性があり、ここではcoqtopはありませんatm）

destruct (Aeq_dec x a);
[ subst; elim (n eq_refl)
| right; apply (IHxs H)
].

（if <foo>は多かれ少なかれ同じmatch <foo> withです。一致を決定できるように（、、 ...）を減らす必要があります（または、の場合はdestruct、任意のタイプの最初または2番目のコンストラクターに減らす必要があります。で再使用します。）ほとんどの場合、ケース分析される値が必要になります（ただし、ここにはありません）。必要な場合は、直接破棄するのではなく、実行してください。）caseifremember (<value>) as foo; destruct foo

于 2011-10-30T17:01:19.130 に答える