문자열에 대한 증명이

Question

'reflexivity'속성을 문자열에 증명하고 싶습니다. 증거를 어떻게 진행할 수 있는지 제발 도와주세요.

Fixpoint beq_str (sa sb : String.string) {struct sb}: bool := 
    match sa, sb with 
| EmptyString, EmptyString => true 
| EmptyString, String b sb' => false 
| String a sa', EmptyString => false 
| String a sa', String b sb'=> match (ascii_dec a b) with 
           | left _ => beq_str sa' sb' 
           | right _ => false 
           end 
end. 
(* compares two string names [n1] and [n2] of type [id'] - returs bool. *) 
Definition beq_names n1 n2 := 
    match (n1, n2) with 
    (name s1, name s2) => beq_str s1 s2 
    end. 

Theorem reflexivty : forall i, 
    true = beq_str i i. 
Proof. 
    intros. induction i. 
    auto. simpl. Admitted. 

Answer 1

확실하지 경우 숙제 또는 독립적 인 연구 ...

Theorem beq_str_refl : forall i, 
    true = beq_str i i. 
Proof. 
    induction 0; simpl; try (rewrite <- IHi; case (ascii_dec a a)); 
    try reflexivity; intro C; elimtype False; apply C; reflexivity. 
Qed. 

이 작동합니다 : 여기 내 코드입니다.

숙제이고 게으르다면 교사가이 문제를 거부 할 것입니다. 자신을 이해하고 증명하기를 원한다면, 필요한 빌딩 블록이 거기에 있고, 그냥 분해하고 현재의 증명 상태로 조각을 던져 넣으십시오.

이 증거에는 두 가지 이상한 점이 있습니다. 첫 번째는 (ascii_dec a a)을 제거합니다. (a의 사례 분석은 작동하지 않습니다.) 전체 사례 (즉, (ascii_dec a a))에 대한 사례 분석을 수행하여 두 개의 부표 (가설 a = a을 추가하고 다른 하나는 a <> a)을 얻습니다.

두 번째 문제는 이전에 해본 적이없는 한 모순과 관련이있을 수 있습니다.

a <> a은 a = a -> False과 같습니다. a = a은 정의에 의해 true이며, False 유형의 값을 구성 할 수 있습니다 (모순 - False에는 생성자가 없음). 이렇게하면 현재 목표를 버릴 수 있습니다 (true = false은 증명할 수 없습니다). 불가능한 것은 False 값으로 구성하십시오.

elimtype False을 입력하면 케이스 분석을 진행하려는 Coq에게 False을 알립니다. False에는 생성자가 없으므로 값이 False 인 단일 목표를 갖습니다. 일반적으로 그것은 불가능할 것이지만, 당신은 당신의 가설들 사이에 모순이 있습니다. apply이 모순 (위의 증명 스크립트에 C으로 이름 지어 짐)은 reflexivity 다음에 표시되는 a = a으로 표시됩니다.

Theorem beq_str_refl : forall i, true = beq_str i i. 
    intro i. induction i as [ | a i IHi ]. 
    (* base case: Empty String *) reflexivity. 
    (* inductive case: *) simpl. rewrite <- IHi. 
     (* do case analysis on ascii_dec (or {a=a}+{a<>a}) *) 
     destruct (ascii_dec a a) as [ Heq | C ]. 
     (* {a = a} *) reflexivity. 
     (* {a <> a} *) unfold not in C. elimtype False. apply C. reflexivity. 

모순을 처리하는 또 다른 방법 : 솔루션에 대한

(* just a quick nonsensical goal *) 
Theorem foo: forall i, i <> i -> 2 + 2 = 5. 
    intros i C. 
    (* explicitly construct a 'False' value *) 
    assert False as H. 
    apply C. reflexivity. 
    (* 'inversion' generates one goal per possible constructor *) 
    (* as False has no constructors, this gives 0 subgoals, finishing the proof *) 
    inversion H. 
Qed.