Странные доказательства обязательств, вытекающих из оценки толчка / популярности в Coq - PullRequest
Новая
       50

Странные доказательства обязательств, вытекающих из оценки толчка / популярности в Coq

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

Я пытаюсь определить простой язык на основе стека в Coq. На данный момент набор инструкций содержит push, который выдвигает nat, и инструкцию pop, которая высовывает единицу. Идея состоит в том, что программы типизированы зависимо; Prog 2 - это программа, которая оставляет два элемента в стеке после выполнения.

Это реализовано с помощью этой простой программы: 

Require Import Coq.Vectors.VectorDef.

Inductive Prog : nat -> Type :=
  | push : forall n : nat, nat -> Prog n -> Prog (S n)
  | pop  : forall n : nat, Prog (S n) -> Prog n.

Fixpoint eval (n : nat) (p : Prog n) : t nat n :=
  match p with
  | push _ n p => cons _ n _ (eval _ p)
  | pop _ p => match eval _ p with
    | cons _ _ _ stack => stack
    end
  end.

Теперь я хочу добавить инструкцию pop', которая извлекает элемент из стека, но может применяться только тогда, когда в стеке есть хотя бы два элемента. 

Inductive Prog : nat -> Type :=
  | push : forall n : nat, nat -> Prog n -> Prog (S n)
  | pop' : forall n : nat, Prog (S (S n)) -> Prog (S n).

При использовании того же Fixpoint, как указано выше (изменение pop на pop'), я получаю ошибку

Термин "стек" имеет тип "t nat n0", в то время как ожидается, что он будет иметь тип "t nat (S k)".

Так что я думал, что смогу сделать это с Program. Поэтому я использую: 

Require Import Coq.Program.Tactics Coq.Logic.JMeq.

Program Fixpoint eval (n : nat) (p : Prog n) : t nat n :=
  match p with
  | push _ n p => cons _ n _ (eval _ p)
  | pop' k p => match eval _ p with
    | cons _ l _ stack => stack
    | nil _ => _
    end
  end.

Однако по какой-то причине это порождает странные обязательства, которые, я не думаю, могут быть решены. Первое (из двух) обязательство, оставшееся после автоматических попыток: 

k : nat
p0 : Prog (S k)
p : Prog (S (S k))
Heq_p : JMeq (pop' k p) p0
l, n0 : nat
stack : t nat n0
h : nat
t : t nat n0
Heq_anonymous0 : JMeq (cons nat l n0 stack) (cons nat h n0 t)
______________________________________(1/1)
n0 = S k

Я не вижу способа связать k, который является аргументом типа для Prog, и n0, который является аргументом типа для векторного типа t.

Почему это Program приводит к этой странной обязанности, и как я могу написать функцию оценки, обходящую эту проблему?

Ответы [ 3 ]

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

Прежде чем ответить на ваш вопрос, обратите внимание, что невозможно написать какую-либо программу на вашем языке!(Это не оказывает никакого влияния на проблему, которую вы описываете, но все равно стоит указать на нее ...) 

From Coq Require Import Vectors.Vector.

Set Implicit Arguments.

Inductive Prog : nat -> Type :=
  | push : forall n : nat, nat -> Prog n -> Prog (S n)
  | pop' : forall n : nat, Prog (S (S n)) -> Prog (S n).

Fixpoint not_Prog n (p : Prog n) : False :=
  match p with
  | push _ p' => not_Prog p'
  | pop'   p' => not_Prog p'
  end.

Теперь к вашему вопросу.Именно из-за этого и связанных с этим проблем многие люди предпочитают избегать такого стиля программирования в Coq.В этом случае мне проще запрограммировать вашу функцию, используя tl, который извлекает хвост вектора. 

From Coq Require Import Vectors.Vector.

Set Implicit Arguments.

Inductive Prog : nat -> Type :=
  | empty : Prog 0
  | push : forall n : nat, nat -> Prog n -> Prog (S n)
  | pop' : forall n : nat, Prog (S (S n)) -> Prog (S n).

Fixpoint eval (n : nat) (p : Prog n) : t nat n :=
  match p with
  | empty    => nil _
  | push n p => cons _ n _ (eval p)
  | pop'   p => tl (eval p)
  end.

Если вы все еще заинтересованы в работе с этим типом данных в Coq, выВозможно, вы захотите взглянуть на плагин Equations , который обеспечивает лучшую поддержку для сопоставления зависимых шаблонов.

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

Вот попытка использования уравнений. 

From Coq Require Import Vector.
From Equations Require Import Equations.

Equations eval (n : nat) (p : Prog n) : t nat n :=
  eval _ (push _ n p) := cons n (eval _ p);
  eval _ (pop' _ p) <= eval _ p => {
    eval _ (pop' _ p) (cons _ stack) := stack }.

Но учтите, что я не совсем уверен в том, что я делаю.

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

Я не смог заставить Program Fixpoint запомнить подходящее равенство, но вот определение, использующее тактику, где мы можем использовать remember, чтобы создать образец конвоя вокруг доказательства равенства.Два подкрепления в проверочном члене были сгенерированы как abstract;оба они действительно простые доказательства о конструкторах. 

Fixpoint eval (n : nat) (p : Prog n) : t nat n.
  refine (match p with
          | push n' v p' => cons _ v _ (eval _ p')
          | pop' n' p' => _
          end).
  set (x := eval _ p').
  remember (S (S n')).
  destruct x.
  abstract congruence. (* nil case *)
  assert (n0 = S n') by (abstract congruence).
  rewrite H in x.
  exact x.
Defined.

Print eval.
(*
eval =
fix eval (n : nat) (p : Prog n) {struct p} :
t nat n :=
  match p in (Prog n0) return (t nat n0) with
  | push n' v p' => cons nat v n' (eval n' p')
  | pop' n' p' =>
      let x := eval (S (S n')) p' in
      let n0 := S (S n') in
      let Heqn0 : n0 = S (S n') := eq_refl in
      match
        x in (t _ n1)
        return (n1 = S (S n') -> Prog n1 -> t nat (S n'))
      with
      | nil _ =>
          fun (Heqn1 : 0 = S (S n')) (_ : Prog 0) =>
          eval_subproof n' Heqn1
      | cons _ _ n1 x0 =>
          fun (Heqn1 : S n1 = S (S n')) (_ : Prog (S n1)) =>
          let H : n1 = S n' := eval_subproof0 n' n1 Heqn1 in
          let x1 :=
            eq_rec n1 (fun n2 : nat => t nat n2) x0 (S n') H in
          x1
      end Heqn0 p'
  end
     : forall n : nat, Prog n -> t nat n
*)
...