J-Bob に会いにジャンピング土下寝

環境構築ってなんでこんなに大変なんだろうね。

## 結論

ちょっと古い DrRacket 7 系を使うことで、Scheme 版も ACL2 版？もとりあえず動いてるような気持ちにはなれた。

### 参考

https://qiita.com/fujim2/items/1a6fae6d49753cef09ba

## 動機

定理を証明していきたくなってきた。Coq はなんだか大変そうだ。
そんな我々に the-little-prover。
和書もあるよ (さすがラムダノート！俺たちに出来ないことを平然とやってのける。ありがとうございます。)
http://the-little-prover.github.io/
https://www.lambdanote.com/collections/littleprover

### 状況

右も左もわかっていない。

とりあえず J-Bob を探してあちこち尋ねたところ、 Racket 8 系で Dracula を入れようとしても無理ということはわかった。

### dracula、どうしてしまったんや

Racket 8 系で Dracula を入れようとすると何となく入りそうなそぶりを見せるのだが、どうもふがふが言ってうまく入らない。

Racket 7 系まではとりあえず動いていたようで、8 系で出力されているエラーをチラ見した感じでは、そこはかとなく

この辺 (vv7.9 ってなんだ？) と
https://github.com/racket/htdp/releases/tag/vv7.9
https://github.com/racket/htdp/releases/tag/v7.9

この辺で、
https://github.com/racket/htdp/releases/tag/v8.0

生じたパスの構成変更に dracula が追従できていなさそうな気がした。
他にも問題があるのかないのかは不明。

https://github.com/carl-eastlund/dracula/issues/7

というイシューで言及されているのと同様のログが手元の Racket 8.4 (Windows 環境) でも見受けられた。

実際、
https://github.com/racket/htdp/blob/vv7.9/htdp-lib/test-engine/scheme-gui.rkt

というファイルは htdp 7 系にはあったようだが、

https://github.com/racket/htdp/tree/v8.0/htdp-lib/test-engine

にはそういうのは見つからない。

これがどういう状況なのかわからないが、とりあえず面倒だから Racket 7.9 を入れたら何事もなかったかのように環境は構築できた。できた？
ような気がするのでとりあえずよし。

### Racket 使うなら

これでいいんじゃね？的な PR も観測されたが詳細不明。

https://github.com/the-little-prover/j-bob/pull/14

## で、どうなってるか

結局 scheme ベースの方でちょこちょこ見ている (Dracula とは何だったのか、、、)。

```scheme:chapter1.scm
;; Load the J-Bob language:
(load "j-bob-lang.scm")
;; Load J-Bob, our little proof assistant:
(load "j-bob.scm")
;; Load the transcript of all proofs in the book:
(load "little-prover.scm")

(J-Bob/step (prelude)
  '(car (cons 'ham '(eggs)))
  '())


(J-Bob/step (prelude)
  '(car (cons 'ham '(eggs)))
  '((() (car/cons 'ham '(eggs)))))

(chapter1.example1)
```

```scheme:output
(car (cons 'ham '(eggs)))
'ham
'ham
```

### `'` は？

`'` が一個ずつ少ないような気がしてるのだけど、どうも Racket 的には暗黙の quotation があったりなかったり？

https://docs.racket-lang.org/reference/quote.html

> Many forms are implicitly quoted (via #%datum) as literals. 

この理解が正しいか自信ないが、出力の設定をいじると quote の存在がうっすらうかがえた (そういう話ではないかもしれないが)。

- Output Style: Constructor

![image.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/616231/55a7c69c-4e61-bf44-f621-8ce8d2895f7f.png)

![image.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/616231/2199dd51-3982-904d-c7f5-a7e402580b50.png)


- Output Style: write (これだと、ぬるっと `'` が一つ足りないように見える。気がする)

![image.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/616231/4583f1e5-3b96-0def-6dbe-b523fc1137e5.png)

<img src="https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/616231/5020e4c6-da61-0f60-429e-8e13514a5db8.png" width=400px>

- Output Style: print

![image.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/616231/64ab7706-167a-95cb-5b1b-5f9eee04dbcb.png)

![image.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/616231/714b271c-1d80-73c7-ce9a-d16d55f351e2.png)


Racket の話ではなく、R5RS の仕様の話とかなのかな？？

https://docs.racket-lang.org/r5rs/r5rs-std/r5rs-Z-H-7.html#%_sec_4.1.2

> 4.1.2  Literal expressions
> ```scheme
> syntax:  (quote <datum>) 
> syntax:  '<datum> 
> syntax:  <constant> 
> ```
> (quote \<datum>) evaluates to \<datum>. \<Datum> may be any external 
> representation of a Scheme object (see section 3.3). This notation is used 
> to include literal constants in Scheme code.
> 
> ```scheme
> (quote a)                             ===>  a
> (quote #(a b c))             ===>  #(a b c)
> (quote (+ 1 2))                       ===>  (+ 1 2)
> ```
> 
> (quote \<datum>) may be abbreviated as '\<datum>. The two notations are 
> equivalent in all respects.
> 
> ```scheme
> 'a                           ===>  a
> '#(a b c)                   ===>  #(a b c)
> '()                          ===>  ()
> '(+ 1 2)                     ===>  (+ 1 2)
> '(quote a)                   ===>  (quote a)
> ''a                          ===>  (quote a)
> ```
>
> Numerical constants, string constants, character constants, and boolean 
> constants evaluate ``to themselves''; they need not be quoted.
> 
> ```scheme
> '"abc"             ===>  "abc"
> "abc"              ===>  "abc"
> '145932            ===>  145932
> 145932             ===>  145932
> '#t          ===>  #t
> #t           ===>  #t
> ```
> 
> As noted in section 3.4, it is an error to alter a constant (i.e. the 
> value of a literal expression) using a mutation procedure like set-car! or string-set!.

https://docs.racket-lang.org/reference/quote.html#%28form._%28%28quote._~23~25kernel%29._quote%29%29

> (quote datum)

> Produces a constant value corresponding to datum (i.e., the representation of the program fragment) without its lexical information, source location, etc. Quoted pairs, vectors, and boxes are immutable.


わかんねー。

#### おまけ

proof pad というのでブラウザで ACL2 をお試しできるらしい。でも http。
http://new.proofpad.org/