induction

2熱

1答えて

2つの固定点定義を含む一見単純な補助定理に苦しんでいます。次の二つの軸方向カラーライブラリからの定義は以下のとおりです。 From Coq Require Import Vector Program. Import VectorNotations. Program Fixpoint Vnth {A:Type} {n} (v : t A n) : forall i, i < n -> A :=

-1熱

2答えて

haskellで帰納的証明を設定するには？

私は、xsはintの有限リストであるwhenver f (g xs) == g (f xs) を証明する必要があります。 fとgの両方がタイプ[INT]であると仮定 - [INT]>反例による

2熱

1答えて

Leanは、再帰型引数を非再帰型引数の後に表示するように強制するのはなぜですか？

次の定義は、リーンによって拒否されます。エラーメッセージと inductive natlist | nil : natlist | cons: natlist → ℕ → natlist 「『natlist.cons』の＃2引数は再帰的ではありませんが、それは再帰的な引数の後起こる」をそして、次の定義が期待どおりに受け入れられます。 inductive natlist | nil :

0熱

1答えて

big-Oの正式な定義を使ってこれを証明する方法は？

big-Oの正式な定義を使ってn^1000000 = O（1.000001^n）を証明したいと思います。私は、これを、誘導による証拠または矛盾による証拠を使って行うことができるかどうか疑問に思っていました。私はまた、制限を使用せずにこれをしたいと思います。

0熱

1答えて

Isabelleでルール誘導と変数一般化を組み合わせるにはどうすればよいですか？

イザベルでは、arbitraryキーワードを使用して、誘導プルーフの変数を一般化できます。これは間違いなく普通の誘導のために働きます。apply (induction n arbitrary: m)のように。私はapply (induction rule: R.induct)のようにルールの誘導をすることもできます。しかし、ルール誘導を使用するときに、どのように変数を一般化できますか？私の特定の

1熱

1答えて

誘導規則のケース名（Isabelle）

一部の誘導規則には大文字と小文字の区別があります。デフォルトの規則の例は、case 0とcase (Suc n)です。与えられた規則、例えば。 int_induct、この補助定理を含む理論を見ずに、どのようにして（実際にはそれがあるのか）そのケースの名前を知ることができますか？

0熱

1答えて

Coqの変数のペアで共同で再帰することは可能ですか？

のは、私は、次のことを証明しようとしているとしましょう： Theorem le_s_n : forall n m, S n <= S m -> n <= m. ペア(n, m)に誘導を行うために生産的であるかもしれないように私は感じます。その場合は、(0, 0),(0, S m'),(S n', 0など）、(S n', S m')のようなものになります。これはすべて可能ですか？

2熱

1答えて

単純型のラムダ計算の閉じた項の自由変数の帰納仮説

単純な型のラムダ計算をCoqで形式化しようとしています。空のコンテキストは空です。これは正式化の関連部分です。 Require Import Coq.Arith.Arith. Require Import Coq.MSets.MSets. Require Import Coq.FSets.FMaps. Inductive type : Set := | tunit : type |

1熱

2答えて

イザベルで誘導的に定義された関係の非再帰性をどのように証明できますか？

はイザベルの例として、自然数の不平等の次の定義を考えてみましょう： inductive unequal :: "nat ⇒ nat ⇒ bool" where zero_suc: "unequal 0 (Suc _)" | suc_zero: "unequal (Suc _) 0" | suc_suc: "unequal n m ⟹ unequal (Suc n) (

1熱

2答えて

Coqベクトルの置換

Coqのベクトルの順列について、私は理由を考える必要があります。標準ライブラリには、リストの置換定義のみが含まれています。私の最初の試みとして、私はのようなベクターのためにそれを模倣しようとした： Inductive VPermutation: forall n, vector A n -> vector A n -> Prop := | vperm_nil: VPermutation