私は、ほとんど自明に見えるこれらの証明に問題があります。
たとえば、帰納的なケースで、タイトルのプロパティを想定して表示したい場合:
length (h'::h::l) = 1 + length (h::l)
ここからどこへ行けばいいですか？それは明らかに真実ですが、ある種の補題を証明せずにどのような手順を踏むことができるかわかりません。たとえば、私は言うことができます
length ([h']@(h::l)) = 1 + length (h::l)
しかし今、私は次の線に沿って何かを証明しなければなりません
length (l1@l2) = length l1 + length l2
補題を証明する必要があるとき、特にほとんど自明に見える証明では、理解に苦しんでいます。
まず、長さは帰納法によって定義され、空隙の長さは 0 であり、長さ (h::l) = 1 + 長さ (l) です。
次に、帰納法、[]@l=l、および [h]@l = h::l によって連結も定義されます。
length は @ を + にマップする関数です: 証明は上記のプロパティを使用した帰納証明です。l1 の帰納法によって進みます: l1 が空の場合、プロパティ length(l1@l2) = length(l1)+length(l2) (帰納公理)。次に、長さ n の l1 に対してプロパティが正しいと仮定すると、n+1 に対して正しいことを証明したいとします。length(h::l1@l2) = 1 + length(l1@l2) (thx から長さの定義)。次に、帰納法の仮説により、長さ(l1@l2) = 長さ(l1)+長さ(l2)と結論付けます。