Изменение, работа и применение выражений let в Coq - PullRequest
Новая
       116

Изменение, работа и применение выражений let в Coq

1 голос
/ 04 мая 2020

Я не уверен, как применить выражение let в coq. Это из примера сортировки выбора в PF.

Как только функция выбора определена, эта лемма доказана. 

Lemma select_perm: forall x l,
  let (y,r) := select x l in
   Permutation (x::l) (y::r).

Вот некоторые примеры использования, чтобы увидеть, как она работает. 

Compute select_perm  3 [10;32;4;6;5].
     = select_perm 3 [10; 32; 4; 6; 5]
     : let (y, r) := select 3 [10; 32; 4; 6; 5] in
       Permutation [3; 10; 32; 4; 6; 5] (y :: r)

Compute select 3 [10; 32; 4; 6; 5].
  = (3, [10; 32; 4; 6; 5])
       : nat * list nat

Как я могу далее оцените это, чтобы раскрыть фактическую перестановку - что-то вроде Compute ((select_perm 3 [10;32;4;6;5]) (select 3 [10; 32; 4; 6; 5]))?

Я не уверен, как использовать эту лемму при применении приведенной ниже теоремы. 

Lemma selsort_perm:
  forall n,
  forall l, length l = n -> Permutation l (selsort l n).
Proof.
  intros.
  generalize dependent n.
  induction l; intros.
  - subst.
    simpl.
    constructor.
  - subst. simpl.
    destruct (select a l) eqn:?.

С соответствующие цели, я хочу как-то применить select_perm (apply (select_perm a l)). 

  a : nat
  l : list nat
  IHl : forall n : nat, length l = n -> Permutation l (selsort l n)
  n : nat
  l0 : list nat
  Heqp : select a l = (n, l0)
  ============================
  Permutation (a :: l) (n :: selsort l0 (length l))

или, соответственно, доказать через транзитивность assert (Permutation (a :: l) (n :: l0)) и каким-то образом привести следующий Heqp в выражение let с новой целью , Существует ли простой способ обработки выражений let, таких как применение функции в coq?

Редактировать:

Я нашел альтернативное решение adho c, изменив select_perm на select_perm'

Lemma select_perm': forall x l,
   Permutation (x::l) ((fst (select x l)) :: (snd (select x l))).

И ввод по всей длине списка, а не самого списка (может предоставить этот код при необходимости), но скорее просто использует оригинальное определение Аппеля ...

1 Ответ

1 голос
/ 05 мая 2020

Да, это сложный вопрос. Вот структура, которую я предлагаю. Чтобы сделать работоспособный, собственный пример, я просто предполагаю существование функций select и selsort и отношения Permutation.

Я фактически привожу в своей цели пример теоремы о том, что я wi sh для использования (как вы предложили), а затем я могу переписать с Heqp. Последние две строки - это то, где все происходит на самом деле. 

Require Import List.

Section playground.

Variable select : nat -> list nat -> nat * list nat.

Variable Permutation : list nat -> list nat -> Prop.

Lemma select_perm: forall x l,
  let (y,r) := select x l in
   Permutation (x::l) (y::r).
Proof.
Admitted.

Variable selsort : list nat -> nat -> list nat.

Lemma goal_at_hand (a : nat) (l : list nat)
  (IHl : forall n : nat, length l = n -> Permutation l (selsort l n))
  (n : nat) (l0 : list nat) (Heqp : select a l = (n, l0)):
  Permutation (a :: l) (n :: selsort l0 (length l)).
Proof.
generalize (select_perm a l).
rewrite Heqp.

Хитрость заключается в том, что Coq использует синтаксис let ... := ... in ..., но на самом деле это выражение сопоставления с образцом: вам нужно, чтобы выражение было явно применение конструктора pair для выражения let для преобразования себя в более простую форму.

Полученная цель имеет следующую форму, я полагаю, вам нужна лемма о том, что Permutation является переходным продолжить. 

  Permutation (a :: l) (n :: l0) ->
  Permutation (a :: l) (n :: selsort l0 (length l))
...