Как сделать оператор else в функциональном языке программирования Coq? - PullRequest
Новая
       4

Как сделать оператор else в функциональном языке программирования Coq?

0 голосов
/ 22 января 2019

Я пытаюсь посчитать количество вхождений элемента v в natlist/bag в Coq. Я попробовал: 

Fixpoint count (v:nat) (s:bag) : nat :=
  match s with
  | nil => 0
  | h :: tl => match h with
               | v => 1 + (count v tl)
               end
  end.

однако мое доказательство не работает: 

Example test_count1:              count 1 [1;2;3;1;4;1] = 3.
Proof. simpl. reflexivity. Qed.

Почему не работает первый фрагмент кода? Что он делает, когда v не совпадает?

Я тоже пробовал: 

Fixpoint count (v:nat) (s:bag) : nat :=
  match s with
  | nil => 0
  | h :: tl => match h with
               | v => 1 + (count v tl)
               | _ => count v tl
               end
  end.

но это также дает ошибку в Coq, и я даже не могу ее запустить.

Функциональное программирование является для меня чем-то новым, поэтому я не знаю, как на самом деле выразить это в Coq. Я действительно просто хочу сказать, если h соответствует v, тогда сделать +1 и рекурсировать только рекурсивный (т.е. добавить ноль, я думаю).

Есть ли простой способ выразить это на функциональном языке программирования Coq?

Причина, по которой я спрашиваю, состоит в том, что мне кажется, что сопоставление очень похоже на оператор if else в "нормальном" программировании на Python. Так что я либо упускаю суть функционального программирования, либо чего-то такого. Это основной вопрос, который меня беспокоит, я думаю, неявно.

Ответы [ 2 ]

0 голосов
/ 22 января 2019

(это похоже на ответ Даниэля, но я уже написал большую часть)

Ваша проблема в том, что в этом коде: 

match h with
| v => 1 + (count v tl)
end

совпадение с v связывает new переменную v. Чтобы проверить, равен ли h v, вам придется использовать некоторую процедуру принятия решения для проверки равенства натуральных чисел.

Например, вы можете использовать Nat.eqb, который принимает два натуральных числа и возвращает bool, указывающий, равны ли они. 

Require Import Nat.

Fixpoint count (v:nat) (s:bag) : nat :=
  match s with
  | nil => 0
  | h :: tl => if (eqb h v) then (1 + count v t1) else (count v t1)
  end.

Почему мы не можем просто соответствовать термину, который хотим? Сопоставление с образцом всегда совпадает с конструкторами типа. В этом фрагменте кода внешний оператор соответствия совпадает с nil и h :: t1 (что является обозначением для cons h t1 или чем-то подобным, в зависимости от точного определения bag). В заявлении о совпадении типа 

match n with
| 0 => (* something *)
| S n => (* something else *)
end.

мы сопоставляем конструкторы для nat: 0 и S _.

В исходном коде вы пытаетесь найти соответствие на v, который не является конструктором, поэтому Coq просто связывает новую переменную и вызывает ее v.

0 голосов
/ 22 января 2019

Оператор match, который вы пытались написать, на самом деле просто затеняет переменную v новой переменной, также называемой v, которая содержит только копию h.

.два натуральных числа равны, вы можете использовать Nat.eqb, который возвращает значение bool, с которым затем можно сопоставить: 

Require Import Arith.

Fixpoint count (v:nat) (s:bag) : nat :=
  match s with
  | nil => 0
  | h :: tl => match Nat.eqb v h with
               | true => 1 + (count v tl)
               | false => count v tl
               end
  end.

Как это происходит, для сопоставления значений bool с trueили false, Coq также предоставляет синтаксический сахар в форме функциональной конструкции if / else (которая очень похожа на троичный оператор ?: из C или C ++, если вы знакомы с любым из них):

Require Import Arith.

Fixpoint count (v:nat) (s:bag) : nat :=
  match s with
  | nil => 0
  | h :: tl => if Nat.eqb v h then
                 1 + (count v tl)
               else
                 count v tl
  end.

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

В общем, однако, для универсального типа не обязательно будет способ решить, являются ли двачлены этого типа равны или нет, как было Nat.eqb в случае nat.Поэтому, если вы хотите написать обобщение count, которое могло бы работать для более общих типов, вам нужно было бы принять аргумент, определяющий процедуру принятия решения о равенстве.

...