Докажите равенство в списке, построенном с помощью карты - PullRequest
Новая
       16

Докажите равенство в списке, построенном с помощью карты

1 голос
/ 25 марта 2020

У меня есть два списка, один из которых построен непосредственно с помощью рекурсии, а другой - с использованием операции карты. Я пытаюсь показать, что они равны, и удивительно, я застрял. 

Require Import Coq.Lists.List.
Import ListNotations.

Fixpoint ls_zeroes n :=
  match n with
  | 0 => nil
  | S n' => 0 :: ls_zeroes n'
  end.

Fixpoint ls_ones n := map S (ls_zeroes n).
Fixpoint ls_ones' n :=
  match n with
  | 0 => nil
  | S n' => 1 :: ls_ones' n'
  end.

Goal forall n, ls_ones n = ls_ones' n.
Proof.
  intros.
  induction n.
  - reflexivity.
  - simpl. f_equal. (* ??? *)
Abort.

Вот как выглядит контекст: 

1 subgoal
n : nat
IHn : ls_ones n = ls_ones' n
______________________________________(1/1)
map S (ls_zeroes n) = ls_ones' n

Я думал, fold ls_ones будет map S (ls_zeroes n) в ls_ones n, поскольку это буквально определение ls_ones, но оно ничего не делает. Если я попытаюсь unfold ls_ones in IHn, то получу противное рекурсивное выражение вместо дословного определения ls_ones.

Какой самый простой способ завершить это доказательство?

Ответы [ 3 ]

2 голосов
/ 25 марта 2020

Обратите внимание, что когда вы определяете ls_one и разворачиваете определение, вы получаете: 

(fix ls_ones (n0 : nat) : list nat := map S (ls_zeroes n0)) n = ls_ones' n

Проблема в том, что ls_one не является точкой фиксации. Действительно, это не делает рекурсию. Как только coq автоматически определяет точку {struct n0} (в этом случае аргумент n), ваше доказательство застревает, потому что n никогда не разрушается в P k -> P (k + 1) , потому что k не разрушен. Использование: 

Definition ls_ones n := map S (ls_zeroes n).

Доказательство становится тривиальным: 

Goal forall n, ls_ones n = ls_ones' n.
Proof.
  intros.
  induction n.
  trivial.
  unfold ls_ones in *.
  simpl.
  rewrite IHn.
  trivial.
Qed.
1 голос
/ 25 марта 2020

К сожалению, из-за значения, зафиксированного в ваших определениях, вы должны использовать индукцию для доказательства: 

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Fixpoint seq0 n :=
  match n with
  | 0 => nil
  | S n' => 0 :: seq0 n'
  end.

Fixpoint seq1 n :=
  match n with
  | 0 => nil
  | S n' => 1 :: seq1 n'
  end.

Lemma eq_F n : seq1 n = [seq n.+1 | n <- seq0 n].
Proof. by elim: n => //= n ->. Qed.

Доказательств не так много. Я бы рекомендовал использовать более общую функцию nseq count elem вместо определения ваших собственных дублирующих структур, тогда доказательство довольно быстро следует из общей леммы о map: 

Lemma eq_G n : nseq n 1 = [seq n.+1 | n <- nseq n 0].
Proof. by rewrite map_nseq. Qed.
1 голос
/ 25 марта 2020

Я думал, fold ls_ones превратится map S (ls_zeroes n) в ls_ones n, поскольку это буквально определение ls_ones

Это так? Вы сказали Fixpoint ls_ones, а не Definition. Как и любой Fixpoint, это означает, что данное определение ls_ones преобразуется в fix. В данном определении нет рекурсивной структуры, так что это бессмысленно, но вы сказали, что делаете это, поэтому Coq делает это. Введите Print ls_ones., чтобы увидеть фактическое определение. Истинное решение состоит в том, чтобы сделать ls_ones a Definition.

Если вы не исправите это, Coq уменьшит Fixpoint, только если рекурсивный аргумент (ы) начинается с конструкторов. Затем, чтобы завершить это доказательство, вам нужно destruct n, чтобы показать эти конструкторы: 

Goal forall n, ls_ones n = ls_ones' n.
Proof.
  intros.
  induction n.
  - reflexivity.
  - simpl. f_equal. destruct n; assumption.
Qed.
...