Omega를 사용하여 Coq에서 보조 정리를 증명합니다.

Question

Omega를 사용하여 Coq에서 증명하려고합니다. 나는 그것에 많은 시간을 보냈지 만, 아무것도 내게 오지 않았다. 나는 내가 코크에서 새로운 사람이라는 것을 말해야 만한다. 그래서 나는 이런 종류의 언어에 익숙하지 않고 많은 경험이 없다. 그러나 나는 그것에 대해 연구 중이다.

Lemma div2_eq : forall n, 2 * div2 n + mod2 n = n. 

그런 다음이 하나를 사용하여 오메가 : 나는 처음 도입이 보조 정리에 의해 증명하기 위해 도움이 될 생각

Require Import Arith Omega. 

Fixpoint div2 (n : nat) := 
match n with 
    S (S p) => S (div2 p) 
| _ => 0 
end. 

Fixpoint mod2 (n : nat) := 
match n with 
    S (S p) => mod2 p 
| x => x 
end. 

이 증거를 만들려면 : 여기

내가 증명해야 코드입니다 및 div2_eq :

Lemma div2_le : forall n, div2 n <= n. 

그러나 나는 더 이상 진행할 수 없었습니다.

누구든지 무엇을 해야할지 알고 있습니까?

Answer 1

당신은 쉽게과 같이 기능 div2 및 mod2에서 유도 원리를 도출 할 수

forall P1, 
    P1 0 0 -> 
    P1 1 0 -> 
    (forall n1, P1 n1 (div2 n1) -> P1 (S (S n1)) (S (div2 n1))) -> 
    forall n1, P1 n1 (div2 n1) 

forall P1, 
    P1 0 0 -> 
    P1 1 1 -> 
    (forall n1, P1 n1 (mod2 n1) -> P1 (S (S n1)) (mod2 n1)) -> 
    forall n1, P1 n1 (mod2 n1) 

이 정리를 적용하려면 사용자가 편리하게 쓸 수 있습니다 :

Functional Scheme div2_ind := Induction for div2 Sort Prop. 
Functional Scheme mod2_ind := Induction for mod2 Sort Prop. 

div2_ind 및 mod2_ind이 더 많거나 적은 유형이 functional induction (div2 n) 또는 functional induction (mod2 n) 일반적으로 induction n이라고 쓸 수 있습니다.

하지만 강한 유도 원리는 이러한 기능과 관련된 :

Lemma nat_ind_alt : forall P1 : nat -> Prop, 
    P1 0 -> 
    P1 1 -> 
    (forall n1, P1 n1 -> P1 (S (S n1))) -> 
    forall n1, P1 n1. 
Proof. 
intros P1 H1 H2 H3. induction n1 as [[| [| n1]] H4] using lt_wf_ind. 
    info_auto. 
    info_auto. 
    info_auto. 
Qed. 

사실은, 어떤 함수의 도메인은 유용한 유도 원리에 대한 단서입니다. 예를 들어, 기능 도메인 plus : nat -> nat -> nat 및 mult : nat -> nat -> nat과 관련된 유도 원리는 구조적 유도 일뿐입니다. 그렇다면 왜 Functional Scheme이 단지 더 일반적인 원칙을 대신 생성하지 않는지 궁금합니다.

은 어떤 경우에도, 귀하의 정리의 증거는 될 :

는

Lemma div2_eq : forall n, 2 * div2 n + mod2 n = n. 
Proof. 
induction n as [| | n1 H1] using nat_ind_alt. 
    simpl in *. omega. 
    simpl in *. omega. 
    simpl in *. omega. 
Qed. 

Lemma div2_le : forall n, div2 n <= n. 
Proof. 
induction n as [| | n1 H1] using nat_ind_alt. 
    simpl. omega. 
    simpl. omega. 
    simpl. omega. 
Qed. 

당신은 기능 유도을 숙지해야하지만, 더 중요한 것은, 당신은 정말 잘 설립 유도을 숙지해야합니다.