Выражение «почти правильность» под опцией типа - PullRequest
Новая
       44

Выражение «почти правильность» под опцией типа

0 голосов
/ 18 февраля 2020

Предположим, у нас есть тип A с отношением эквивалентности (===) : A -> A -> Prop.

Кроме того, есть функция f : A -> option A.

Так получилось, что эта функция f "почти" Proper относительно equiv. Под «почти» я подразумеваю следующее: 

Lemma almost_proper :
  forall a1 a2 b1 b2 : A,
    a1 === a2 ->
    f a1 = Some b1 -> f a2 = Some b2 ->
    b1 === b2.

Другими словами, если f завершается успешно на обоих входах, связь сохраняется, но f может все же завершиться ошибкой на одном и успешно на другом , Я хотел бы express кратко изложить эту концепцию, но при этом у меня возникло несколько вопросов.

Я вижу три решения проблемы:

  1. Оставьте все как есть , Не используйте классы типов, докажите леммы, подобные приведенным выше. Это выглядит не очень хорошо, из-за большого количества предварительных условий, таких как x = Some y, которые создают сложности при доказательстве лемм.

  2. Можно доказать Proper ((===) ==> equiv_if_Some) f, когда equiv_if_Some определяется следующим образом : 

    Inductive equiv_if_Some {A : Type} {EqA : relation A} `{Equivalence A EqA} : relation (option A) :=
| equiv_Some_Some : forall a1 a2, a1 === a2 -> equiv_if_Some (Some a1) (Some a2)
| equiv_Some_None : forall a, equiv_if_Some (Some a) None
| equiv_None_Some : forall a, equiv_if_Some None (Some a)
| equiv_None_None : equiv_if_Some None None.

    Одна из проблем здесь заключается в том, что это больше не отношение эквивалентности (оно не является транзитивным).

  3. Возможно, можно доказать Almost_Proper ((===) ==> (===)) f, если некоторые разумные Almost_Proper класс используется. Я не уверен, как это будет работать.

Каков наилучший способ express этой концепции? Я склоняюсь ко второму, но, возможно, есть еще варианты?

Для вариантов 2 и 3 существуют ли ранее существующие общие имена (и, следовательно, возможно, предварительно созданные определения) для отношений, которые я описываю? (equiv_if_Some и Almost_Proper)

1 Ответ

1 голос
/ 18 февраля 2020

2, если это упрощает ваши доказательства.

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

equiv_if_Some может быть лучше определить как подтекст (аналогично тому, как это выглядит в лемме almost_proper), чем как индуктивный тип.

Вы можете также рассмотреть возможность использования других отношений (в качестве альтернативы или в комбинация с equiv_if_Some):

  • Частичный порядок, который может относиться только None к Some, но не Some к None
  • Отношение частичной эквивалентности , которые могут относиться только к Some с.
...