Как я рассуждаю об условных выражениях в Coq? - PullRequest
Новая
       12

Как я рассуждаю об условных выражениях в Coq?

3 голосов
/ 29 октября 2011

Я работаю через модуль ListSet из стандартной библиотеки Coq. Я не уверен, как рассуждать об условных выражениях в доказательстве. Например, у меня возникли проблемы со следующим доказательством. Определения предоставляются для контекста. 

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 <> x, чтобы получить set_mem xs. Однако я не понимаю, как это сделать. Как мне работать, или разлагать, или применять условные выражения?

1 Ответ

2 голосов
/ 30 октября 2011

Вы пробовали это?(синтаксис может быть ошибочным, здесь нет команды atm) 

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

(if <foo> более или менее совпадает с match <foo> with. Вам придется уменьшить (destruct, case,...) так, чтобы совпадение можно было решить (или для if все должно быть сведено либо к первому, либо ко второму конструктору того типа, с которым вы его используете.) В большинстве случаев вам понадобитсязначение, которое анализируется регистром (хотя и не здесь). Если вам это нужно, сделайте remember (<value>) as foo; destruct foo вместо прямой деструкции.)

...