Используя Omega для доказательства леммы в Coq

Я пытаюсь сделать доказательство в Coq с помощью Omega. Я потратил на это много времени, но мне ничего не пришло. Я должен сказать, что я новичок в Coq, поэтому мне не нравится этот язык, и у меня нет большого опыта. Но я работаю над этим.

Вот код, который мне нужно доказать:

Require Import Arith Omega.

Fixpoint div2 (n : nat) :=
 match n with
   S (S p) => S (div2 p)
 | _ => 0
 end.

Fixpoint mod2 (n : nat) :=
 match n with
   S (S p) => mod2 p
 | x => x
 end.

Чтобы провести это доказательство, я подумал, что будет полезно сначала доказать по индукции эту лемму:

Lemma div2_eq : forall n, 2 * div2 n + mod2 n = n.

Затем этот, используя omega и div2_eq:

Lemma div2_le : forall n, div2 n <= n.

Но дальше пойти не удалось.

Кто-нибудь знает что делать?


induction coq proof
person Flo    schedule 03.12.2012    source источник

Ответы (1)


arrow_upward
4
arrow_downward

Вы можете легко вывести принципы индукции из функций div2 и mod2 следующим образом:

Functional Scheme div2_ind := Induction for div2 Sort Prop.
Functional Scheme mod2_ind := Induction for mod2 Sort Prop.

div2_ind и mod2_ind имеют более или менее типы:

forall P1,
  P1 0 0 ->
  P1 1 0 ->
  (forall n1, P1 n1 (div2 n1) -> P1 (S (S n1)) (S (div2 n1))) ->
  forall n1, P1 n1 (div2 n1)

forall P1,
  P1 0 0 ->
  P1 1 1 ->
  (forall n1, P1 n1 (mod2 n1) -> P1 (S (S n1)) (mod2 n1)) ->
  forall n1, P1 n1 (mod2 n1)

Чтобы применить эти теоремы, вы можете написать functional induction (div2 n) или functional induction (mod2 n) вместо induction n.

Но с этими функциями связан более сильный принцип индукции:

Lemma nat_ind_alt : forall P1 : nat -> Prop,
  P1 0 ->
  P1 1 ->
  (forall n1, P1 n1 -> P1 (S (S n1))) ->
  forall n1, P1 n1.
Proof.
intros P1 H1 H2 H3. induction n1 as [[| [| n1]] H4] using lt_wf_ind.
  info_auto.
  info_auto.
  info_auto.
Qed.

Фактически, определение любой функции является ключом к полезному принципу индукции. Например, принцип индукции, связанный с областью определения функций plus : nat -> nat -> nat и mult : nat -> nat -> nat, является просто структурной индукцией. Это заставляет меня задаться вопросом, почему Functional Scheme вместо этого не просто генерирует эти более общие принципы.

В любом случае доказательства ваших теорем тогда станут:

Lemma div2_eq : forall n, 2 * div2 n + mod2 n = n.
Proof.
induction n as [| | n1 H1] using nat_ind_alt.
  simpl in *. omega.
  simpl in *. omega.
  simpl in *. omega.
Qed.

Lemma div2_le : forall n, div2 n <= n.
Proof.
induction n as [| | n1 H1] using nat_ind_alt.
  simpl. omega.
  simpl. omega.
  simpl. omega.
Qed.

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

person Community    schedule 15.12.2012