coq

0熱度

1回答

我是Coq新手。我感到困惑以下證明： Lemma nth_eq : forall {A} (l1 l2 : list A), length l1 = length l2 -> (forall d k, nth k l1 d = nth k l2 d) ->l1 = l2. Proof. intros. 結果表明： 1 subgoal A : Type l1, l2 : li

7熱度

1回答

程序固定點和Coq中的函數有什麼區別？

他們似乎服務於類似的目的。我注意到的一個區別是，儘管Program Fixpoint將接受像{measure (length l1 + length l2) }這樣的複合測量，但Function似乎拒絕此並且將只允許{measure length l1}。是Program Fixpoint嚴格比Function更強大，還是他們更適合不同的使用情況？

1熱度

1回答

Coq：PartialOrder類型類的使用

我試圖在字符串上定義字典順序，但我不完全確定如何使用類型類型PartialOrder。 Require Import List RelationClasses. Fail Inductive lex_leq {A : Type} `{po : PartialOrder A} : list A -> list A -> Prop := | lnil: forall l, lex_leq

2熱度

1回答

對應於* _rect系列功能的合作原理

定義一個新類型foo給出了遞歸原則foo_rect，其優雅地摘要了fix。是否可以通過「翻轉箭頭」來定義一個合作的等效物（摘自cofix）？

2熱度

1回答

Ltac呼叫「cofix」失敗。錯誤：所有方法都必須構建coinductive類型

元素 Require Import Streams. CoFixpoint map {X Y : Type} (f : X -> Y) (s : Stream X) : Stream Y := Cons (f (hd s)) (map f (tl s)). CoFixpoint interleave {X : Type} (s : Stream X * Stream X) : S

1熱度

1回答

不動點函數類型類實例

我試圖在一個類型的類實例的上下文中使用固定點式的功能，但它似乎並沒有工作。有什麼額外的工作要做嗎？暫時我用移動式類外的函數，並明確聲明它不動點的黑客攻擊。然而，這看起來很糟糕。下面是簡單的例子： Inductive cexp : Type := | CAnd : cexp -> cexp -> cexp | COr : cexp -> cexp -> cexp | CProp : bool

2熱度

1回答

在Coq/SSreflect中排序seq

我目前正在玩coq中的紅黑樹，並希望配備nat的訂單列表，以便使用MSetRBT模塊將它們存儲在紅黑樹上。出於這個原因，如圖所示我已經定義seq_lt： Fixpoint seq_lt (p q : seq nat) := match p, q with | _, [::] => false | [::], _ => true | h :: p', h' :: q'

2熱度

2回答

PHOAS in Coq：type mismatch

我在Coq中抄錄了2008 PHOAS paper第2.1節中的（非正式）定義。 Inductive tm' {V : Set} : Set := | Var : V -> tm' | App : tm' -> tm' -> tm' | Abs : (V -> tm') -> tm'. Definition tm := forall X, @tm' X. Fail Example i

2熱度

2回答

Coq：爲什麼我需要手動展開一個值，即使它有一個'提示Unfold`？

我已經想出了下面玩具證明腳本： Inductive myType : Type := | c : unit -> myType. Inductive myProp : myType -> Type := | d : forall t, myProp (c t). Hint Constructors myProp. Definition myValue : myType := c tt

3熱度

2回答

勒柯克最佳實踐：相互遞歸，只有一個功能，在結構上減少

考慮下面的玩具表現爲無類型演算： Require Import String. Open Scope string_scope. Inductive term : Set := | Var : string -> term | Abs : string -> term -> term | App : term -> term -> term. Fixpoint print (ter