Проблемы с импортом Coq - PullRequest
Новая
       17

Проблемы с импортом Coq

0 голосов
/ 27 апреля 2019

Я пытаюсь импортировать Библиотека Coq.Structures.OrdersFacts как обычно с: 

Require Import Coq.Structures.OrdersFacts

Затем я пытаюсь использовать там леммы с: apply CompareFacts.compare_nlt_iff. илиapply compare_nlt_iff. Но ничего не работает ... что я пропускаю?

1 Ответ

2 голосов
/ 28 апреля 2019

CompareFacts - это Module Type, а не Module. Вы можете видеть это, если вы делаете 

Require Import  Coq.Structures.OrdersFacts.
Print OrdersFacts.CompareFacts.

Найдите модуль этого типа и примените вместо него его леммы.

EDIT:

Я имел в виду, что для использования лемм, т. Е. nat, вам нужен модуль, который показывает, что nat является DecStrOrder' (а Nat из PeanoNat является таким модулем), а также тот, который специализируется CompareFacts на nat.

Возможно, пример более полезен. 

Require Import  Coq.Structures.OrdersFacts.

Module mymodule (O:DecStrOrder') (T: CompareFacts O).
  Import T.
  Import O.
  Check compare_eq_iff. (* from CompareFacts *)

  (* a theorem about terms of type O.t *)
  Lemma lem1 a b c: (a ?= b) = Eq -> b == c -> c == a. 
    intros.
    rewrite compare_eq_iff in H.  (* here we use the lemma *)
    rewrite H.
    rewrite H0.
    apply eq_equiv.
  Qed.
End mymodule.

(* the above module functor can be specialised for i.e. nat *)

Require Import PeanoNat.

Print CompareFacts.
Module M : CompareFacts Nat.
  Definition compare_eq_iff := Nat.compare_eq_iff.
  Definition compare_eq := Nat.compare_eq.
  Definition compare_lt_iff := Nat.compare_lt_iff.
  Definition compare_gt_iff := Nat.compare_gt_iff.
  Definition compare_nlt_iff := Nat.compare_nlt_iff.
  Definition compare_ngt_iff := Nat.compare_ngt_iff.
  Definition compare_refl := Nat.compare_refl.
  Definition compare_compat: Proper (eq==>eq==>eq) Nat.compare.
    intros x y Hxy a b Hab; now subst. Defined.
  Definition compare_antisym := Nat.compare_antisym.
End M.  

Module natmodule := mymodule Nat M.
Check natmodule.lem1.
...