Coq: Beweisen Sie die Gleichheit von zwei Fakultät Funktionen mit Induktion

Question

Ich möchte beweisen, dass zwei Fakultät Funktionen in Coq mit Induktion äquivalent sind.

Der Basisfall n = 0 ist einfach, jedoch ist der Induktionsfall komplizierter. Ich sehe, dass ich fertig wäre, wenn ich (visit_fac_v2 n' (n * a)) zu n * (visit_fac_v2 n' a) umschreiben könnte. Die Übersetzung dieser Idee in Coq verursacht jedoch Probleme.

Wie würde man das in Coq beweisen?

Fixpoint fac_v1 (n : nat) : nat := 
    match n with 
    | 0 => 1 
    | S n' => n * (fac_v1 n') 
    end. 

Fixpoint visit_fac_v2 (n a : nat) : nat := 
    match n with 
    | 0 => a 
    | S n' => visit_fac_v2 n' (n * a) 
    end. 

Definition fac_v2 (n : nat) : nat := 
    visit_fac_v2 n 1. 

Proposition equivalence_of_fac_v1_and_fac_v2 : 
    forall n : nat, 
    fac_v1 n = fac_v2 n. 
Proof. 
Abort. 

Answer 1

A Eine typische Sache zu tun, wenn bewiesen wird, dass eine direkte Stilfunktion und ihr akkumulatorbasiertes Äquivalent gleich sind, besteht darin, eine stärkere Invariante anzugeben, die für jeden Wert, den der Akkumulator halten kann, wahr sein sollte.

Sie können es dann auf den Wert spezialisieren, mit dem die Funktion aufgerufen wird, und so die Anweisung erhalten, an der Sie interessiert sind, als eine Folge des allgemeineren.

Die allgemeine Aussage ist hier wie folgt:

Theorem general_equivalence_of_fac_v1_and_fac_v2 : 
    forall n a : nat, 
    a * fac_v1 n = visit_fac_v2 n a. 

Und sein Beweis ist recht einfach (Sie vorsichtig sein müssen und dafür sorgen, dass induction vor intro a kommt, weil Sie die Induktionsvoraussetzung gültig sein soll für jedea):

Proof. 
intros n; induction n; intro a. 
- simpl ; ring. 
- simpl ; rewrite <- IHn ; ring. 
Qed. 

Ihr Vorschlag ist eine direkte Folge dieser allgemeineren Satzes.

Answer 2

Im induktiven Fall können Sie die Induktionsvoraussetzung anwenden und das Ziel vereinfachen:

visit_fac_v2 n 1 + n * visit_fac_v2 n 1 = visit_fac_v2 n (S n) 

Um dies zu beweisen, können Sie das folgende Lemma:

Lemma visit_fac_v2_extract: 
    forall n a : nat, 
    visit_fac_v2 n a = a * visit_fac_v2 n 1.