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 := match

0열

2답변

유도 단계에서 실수를 찾을 수 없습니다.

몇 일 전 일부 유도 실행을 해결하면서이 문제를 시도하고 해결했습니다. 성명 이 "증명"에 어떤 문제가 있습니까? "정리"모든 양의 정수 n에 대해 x와 y가 max (x, y) = n 인 양의 정수이면 x = y입니다. k를 수 : 기본 단계 : N = 1은 최대 (X, Y) = 1이고, x 및 y는 양의 정수이다 않으면 X = 1, Y = 1 유도 단계

2열

1답변

왜 Lean은 재귀 적 형식 인수를 비 반복적 형식 뒤에 표시 할 것을 강요합니까?

다음 정의는 린에 의해 거부되어 오류 메시지와 inductive natlist | nil : natlist | cons: natlist → ℕ → natlist 에게 " 'natlist.cons'의 2가 순환되지 인수 번호를하지만 재귀 인수 후 발생" 다음과 같은 정의가 예상대로 수용됩니다. inductive natlist | nil : natli

4열

3답변

coq 유도가 동등 함과 일치 함

나는 알려진 값을 가진 목록을 가지고 있으며, 원래 목록이 무엇인지 추적하고, 요소로 참조하기를 원합니다. 다시 말해서, 저는 (... :: l) 대신에 다양한 i를 사용하여 그것을 참조해야합니다. 나는 그렇게하도록 유도 원리를 만들려고 노력했다. 불필요한 정리가 Admitted로 바뀐 프로그램이 있습니다. 목표는 countDown_nth를 사용하여 all

0열

1답변

이사벨에서 규칙 유도와 변수 일반화를 어떻게 결합 할 수 있습니까?

이사벨 (Isabelle)에서는 arbitrary 키워드를 사용하여 유도 증명에 변수를 일반화 할 수 있습니다. 이것은 보통 유도를 위해 확실히 작동합니다 (예 : apply (induction n arbitrary: m)). apply (induction rule: R.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. Induc

10열

1답변

Agda에서 어떤 크기의 유형이 있습니까?

Agda에서 어떤 크기의 유형이 있습니까? MiniAgda에 대한 논문을 읽으려고했으나 다음과 같은 이유로 진행하지 못했습니다. 왜 데이터 형식이 그 크기보다 일반적입니까? 내가 아는 한 크기는 유도 나무의 깊이입니다. 왜 데이터 유형이 크기에 대해 공분합니다 (예 : < = j -> T_i < = T_j? > 및 # 패턴의 의미는 무엇입니까?

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 -> vec