Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: bug_1779.v Sprache: Coq

Original von: Coq^©

Require Import Div2.

Lemma double_div2: forall n, div2 (double n) = n.
exact (fun n =>  let _subcase :=
    let _cofact := fun _ : 0 = 0 => refl_equal 0 in
    _cofact (let _fact := refl_equal 0 in _fact) in
  let _subcase0 :=
    fun (m : nat) (Hrec : div2 (double m) = m) =>
    let _fact := f_equal div2 (double_S m) in
    let _eq := trans_eq _fact (refl_equal (S (div2 (double m)))) in
    let _eq0 :=
      trans_eq _eq
        (trans_eq
           (f_equal (fun f : nat -> nat => f (div2 (double m)))
              (refl_equal S)) (f_equal S Hrec)) in
    _eq0 in
  (fix _fix (__ : nat) : div2 (double __) = __ :=
     match __ as n return (div2 (double n) = n) with
     | 0 => _subcase
     | S __0 =>
         (fun _hrec : div2 (double __0) = __0 => _subcase0 __0 _hrec)
           (_fix __0)
     end) n).
Guarded.
Defined.

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.