Как конвертировать пропозициональных формул к ДНФ в Кок

Я определил свои пропозициональные формулы следующим образом: 

Inductive propForm : Set :=
| top : propForm
| bot : propForm
| var : propVar -> propForm
| orp : propForm -> propForm -> propForm
| andp : propForm -> propForm -> propForm.

Я пытаюсь определить функцию для преобразования пропозициональной формулы в одну в DNF. Для этого я определил функцию, которая распределяет члены, используя закон распределения: 

Fixpoint distribute (f:propForm) : propForm -> propForm :=
fix distribute1 (g:propForm) : propForm :=
match f with
| f1 /p f2 => match g with
            | g1 /p g2 => distribute1 g1 /p distribute1 g2
            | _ => distribute f1 g /p distribute f2 g
            end
| _ => match g with
       | g1 /p g2 => distribute1 g1 /p distribute1 g2
       | _ => f /p g
       end
end.

Эта функция работает нормально. Однако мне все еще нужно определить функцию, которая преобразует пропозициональную формулу в DNF. Следующая функция будет делать то, что я хочу, однако она не принимается Coq, потому что функция структурно не уменьшается в f' для последнего случая. Любые советы и подсказки будут оценены.

Fixpoint toDNF (f':propForm):propForm :=
match f' with
| top => f'
| bot => f'
| var _ => f'
| f1 /p f2 => toDNF f1 /p toDNF f2
| f1 /p f2 => toDNF (distribute f1 f2)
end.
1 2
normalization coq

1 ответ:

Ваша функция является частным случаем нормализации выражения из полукольца. Я написал пост , объясняющий, как это сделать в случае арифметических выражений, используя библиотеки Ssreflect и MathComp, но я включу более прямой ответ здесь.

Одна из идей состоит в том, чтобы использовать списки списков для представления формул в DNF: в конце концов, они являются просто конъюнкцией списка дизъюнкций, которые являются просто списками литералов. Затем вы можете повторно использовать библиотеку списков для записи вашего функция: 
Module Sol1.

Require Import Coq.Lists.List.
Import ListNotations.

Notation propVar := nat.

Inductive propAtom :=
| top | bot | var :> propVar -> propAtom.

Inductive propForm : Set :=
| atom :> propAtom -> propForm
| orp : propForm -> propForm -> propForm
| andp : propForm -> propForm -> propForm.

Definition dnfForm := list (list propAtom).

Fixpoint andd (f1 f2 : dnfForm) : dnfForm :=
  match f1 with
  | [] =>
    (* false && f2 = false *)
    []
  | cf :: f1 =>
    (* (cf || f1) && f2 = cf && f2 || f1 && f2 *)
    map (app cf) f2 ++ andd f1 f2
  end.

Fixpoint toDNF (f : propForm) : dnfForm :=
  match f with
  | atom a => [[a]]
  | orp f1 f2 => toDNF f1 ++ toDNF f2
  | andp f1 f2 => andd (toDNF f1) (toDNF f2)
  end.

Compute (toDNF (andp (orp 3 4) (orp 1 2))).

End Sol1.

Есть две вещи, чтобы отметить здесь. Во-первых, я учел переменные и константы как отдельный тип propAtom, и я назвал distribute andd, потому что вы можете думать об этом как о вычислении и двух выражений в DNF.

Вот еще одно решение, основанное на исходном коде. Похоже, что ваша функция distribute сохраняет инвариант нахождения в DNF; то есть, если f1 и f2 находятся в DNF, то и distribute f1 f2 тоже. Таким образом, вы можете просто перевернуть порядок вызовов: 

Module Sol2.

Notation propVar := nat.

Inductive propForm : Set :=
| top : propForm
| bot : propForm
| var :> propVar -> propForm
| orp : propForm -> propForm -> propForm
| andp : propForm -> propForm -> propForm.

Fixpoint distribute (f:propForm) : propForm -> propForm :=
fix distribute1 (g:propForm) : propForm :=
match f with
| orp f1 f2 => match g with
            | orp g1 g2 => orp (distribute1 g1) (distribute1 g2)
            | _ => orp (distribute f1 g) (distribute f2 g)
            end
| _ => match g with
       | orp g1 g2 => orp (distribute1 g1) (distribute1 g2)
       | _ => andp f g
       end
end.

Fixpoint toDNF (f':propForm):propForm :=
match f' with
| top => f'
| bot => f'
| var _ => f'
| orp f1 f2 => orp (toDNF f1) (toDNF f2)
| andp f1 f2 => distribute (toDNF f1) (toDNF f2)
end.

Compute (toDNF (andp (orp 3 4) (orp 1 2))).

End Sol2.
2