Разложение равенства конструкторов с выражениями соответствия в Coq - PullRequest
Новая
       5

Разложение равенства конструкторов с выражениями соответствия в Coq

0 голосов
/ 01 мая 2018

У меня есть вопрос, похожий на Разложение равенства конструкторов coq , однако мое равенство содержит выражение match. Рассмотрим пример (который бессмыслен, но используется только для пояснения): 

Fixpoint positive (n : nat) :=
  match n with
  | O => Some O
  | S n => match positive n with
    | Some n => Some (S n)
    | None => None (* Note that this never happens *)
    end
  end.

Lemma positiveness : forall n : nat, Some (S n) = positive (S n).
Proof.
intro.
simpl.

На данный момент, с n : nat в окружающей среде, цель: 

Some (S n) =
match positive n with
| Some n0 => Some (S n0)
| None => None
end

Я хочу преобразовать это в две подцели в среде n, n0 : nat: 

positive n = Some n0  (* Verifying the match *)
S n = S n0            (* Verifying the result *)

И я ожидал бы, что если match для доказательства равенства имеет несколько случаев, которые могут сработать, новая цель - это дизъюнкция всех возможностей, например, для 

Some (S n) =
match positive n with
| Some (S n0) => Some (S (S n0))
| Some O => Some (S O)
| None => None
end

Я бы ожидал 

   (positive n = Some (S n0) /\ S n = S (S n0))  (* First alternative *)
\/ (positive n = Some O      /\ S n = S O)       (* Second alternative *)

Есть ли тактика Coq, которая делает это или что-то подобное?

Ответы [ 2 ]

0 голосов
/ 03 мая 2018

Есть ли тактика Coq, которая делает это или что-то подобное?

Если вы запустите destruct (positive n) eqn:H, вы получите две подзадачи. В первом подцеле вы получите: 

  n, n0 : nat
  H : positive n = Some n0
  ============================
  Some (S n) = Some (S n0)

и во второй подцели вы получите 

  n : nat
  H : positive n = None
  ============================
  Some (S n) = None

Это не совсем то, что вы просили, но во второй подцели вы можете написать assert (exists n0, positive n = Some n0); это даст вам цель, к которой вы стремитесь, и вы можете выполнить оставшуюся цель, destruct используя exists и используя congruence или discriminate, чтобы показать, что positive n не может быть None и Some при в то же время.

0 голосов
/ 01 мая 2018

У меня проблемы с пониманием вашей мотивации. В вашем примере легче доказать свой результат с помощью более общей леммы: 

Fixpoint positive (n : nat) :=
  match n with
  | O => Some O
  | S n => match positive n with
    | Some n => Some (S n)
    | None => None (* Note that this never happens *)
    end
  end.

Lemma positiveness n : positive n = Some n.
Proof.
  now induction n as [|n IH]; simpl; trivial; rewrite IH.
Qed.

Lemma positiveness' n : Some (S n) = positive (S n).
Proof. now rewrite positiveness. Qed.

Возможно, анализ ситуации, который вы хотите выполнить, лучше подходит для другого приложения?

...