コラッツ予想がとけたらいいな2

自分の考察を書いていきます。

定理証明手習いをCoqで 第6章

定理証明手習い

定理証明手習い

@suharahiromichi
この文書のソースコードは以下にあります。
https://github.com/suharahiromichi/coq/blob/master/lisp/tlp_lisp_3.v

「The Little Prover」のCoqでの実現

以下のコードを実行するときは、氏のCoqコードを読み込んだ後にお願いします。

リスト型帰納法による証明をおこなう。

(** Chapter6 最後まで考え抜くのです *)

(* 書き換え用に公理を付け足す *)
Variable xs : star.
Variable membE :
  memb (CONS (CAR xs) (remb (CDR xs))) =
    (_IF (ATOM (CONS (CAR xs) (remb (CDR xs))))
         'NIL
         (_IF (EQUAL (CAR (CONS (CAR xs) (remb (CDR xs)))) '?)
              'T
              (memb (CDR (CONS (CAR xs) (remb (CDR xs))))))).
Variable rembE :
  remb xs =
  (_IF (ATOM xs)
       '()
       (_IF (EQUAL (CAR xs) '?)
            (remb (CDR xs))
            (CONS (CAR xs) (remb (CDR xs))))).
Variable EQA : (EQUAL 'NIL 'NIL) = 'T.

Theorem memb_remb :
  ~ ATOM xs -> ATOM xs -> ~ (EQUAL (CAR xs) '?) -> (EQUAL (CAR xs) '?) -> (EQUAL (memb (remb (CDR xs))) 'NIL) ->
    (_IF (ATOM xs)
         (EQUAL (memb (remb xs)) 'NIL)
         (_IF (EQUAL (memb (remb (CDR xs))) 'NIL)
              (EQUAL (memb (remb xs)) 'NIL)
              'T)).
Proof.
  move => H0 H1 H2 H3 H4.
  rewrite rembE.
  rewrite {1}(iffLR ifAP (if_nest_A
    (ATOM xs)
    '()
    (_IF (EQUAL (CAR xs) '?) (remb (CDR xs)) (CONS (CAR xs) (remb (CDR xs))))
  )).
  rewrite membB.
  rewrite atomB.
  rewrite (equal_eq (if_true 'NIL
     (_IF (EQUAL (CAR '()) '?) 'T (memb (CDR '()))))).
  rewrite EQA.

  (* rewrite rembE. *)
  rewrite (iffLR ifEP (if_nest_E
    (ATOM xs)
    '()
    (_IF (EQUAL (CAR xs) '?) (remb (CDR xs)) (CONS (CAR xs) (remb (CDR xs))))
  )).
(* --- ifの持ち上げ --- *)
  rewrite -(equal_eq (if_same
    (EQUAL (CAR xs) '?)
    (memb (_IF (EQUAL (CAR xs) '?) (remb (CDR xs)) (CONS (CAR xs) (remb (CDR xs)))))
  )).
  rewrite {1}(iffLR ifAP (if_nest_A
    (EQUAL (CAR xs) '?)
    (remb (CDR xs))
    (CONS (CAR xs) (remb (CDR xs)))
  )).
  rewrite (iffLR ifEP (if_nest_E
    (EQUAL (CAR xs) '?)
    (remb (CDR xs))
    (CONS (CAR xs) (remb (CDR xs)))
  )).
(* --- ifの持ち上げ --- *)
  rewrite {2}(iffLR ifAP (equal_if (memb (remb (CDR xs))) 'NIL)).
  rewrite membE.
  rewrite (equal_eq (atom_cons (CAR xs) (remb (CDR xs)))).
  rewrite (equal_eq (if_false 'NIL
    (_IF (EQUAL (CAR (CONS (CAR xs) (remb (CDR xs)))) '?)
              'T
              (memb (CDR (CONS (CAR xs) (remb (CDR xs)))))))).
  rewrite (equal_eq (car_cons (CAR xs) (remb (CDR xs )))).
  rewrite (equal_eq (cdr_cons (CAR xs) (remb (CDR xs )))).
  rewrite (iffLR ifEP (if_nest_E
    (EQUAL (CAR xs) '?)
    'T
    (memb (remb (CDR xs)))
  )).
  rewrite {2}(iffLR ifAP (equal_if (memb (remb (CDR xs))) 'NIL)).

  rewrite (equal_eq (if_same (EQUAL (CAR xs) '?) 'NIL)).
  rewrite EQA.
  rewrite (equal_eq (if_same (EQUAL (memb (remb (CDR xs))) 'NIL) 'T)).
  rewrite (equal_eq (if_same (ATOM xs) 'T)).
  done.

  done.
  done.
  done.
  done.
  done.
  done.
  done.
Qed.