Chứng minh rằng một danh sách đảo ngược là một palindrome trong Coq

Question

Dưới đây là định nghĩa của tôi quy nạp của palindromes:

Inductive pal { X : Type } : list X -> Prop := 
    | pal0 : pal [] 
    | pal1 : forall (x : X), pal [x] 
    | pal2 : forall (x : X) (l : list X), pal l -> pal (x :: l ++ [x]). 

Và định lý tôi muốn chứng minh, từ Foundations Software:

Theorem rev_eq_pal : forall (X : Type) (l : list X), 
    l = rev l -> pal l. 

My các phác thảo chính thức của bằng chứng như sau:

Giả sử l0 là một danh sách tùy ý như vậy l0 = rev l0. Sau đó, một trong ba trường hợp sau phải giữ. l0 có:

(a) phần tử không, trong trường hợp đó là palindrome theo định nghĩa.

(b) một phần tử, trong trường hợp đó, nó cũng là palindrome theo định nghĩa.

(c) hai thành phần trở lên, trong trường hợp này là l0 = x :: l1 ++ [x] đối với một số thành phần x và một số danh sách l1 sao cho l1 = rev l1.

Bây giờ, kể từ khi l1 = rev l1, một trong ba trường hợp sau đây phải giữ ...

Phân tích trường hợp đệ quy sẽ chấm dứt đối với bất kỳ danh sách hữu hạn l0 vì độ dài của danh sách đã phân tích giảm bởi 2 thông qua mỗi lần lặp. Nếu nó kết thúc cho bất kỳ danh sách ln, tất cả các danh sách bên ngoài của nó lên đến l0 cũng là palindromes, vì danh sách được xây dựng bằng cách chắp thêm hai phần tử giống nhau ở cuối đầu palindrome cũng là palindrome.

Tôi nghĩ lý do là âm thanh, nhưng tôi không chắc chắn làm thế nào để chính thức hóa nó. Liệu nó có thể trở thành một bằng chứng trong Coq? Một số giải thích về cách chiến thuật sử dụng công việc sẽ đặc biệt hữu ích.

Answer 1

Đây là ví dụ điển hình khi cảm ứng "trực tiếp" không hoạt động tốt vì bạn không trực tiếp thực hiện cuộc gọi đệ quy trên đuôi, nhưng trên phần của đuôi. Trong những trường hợp như vậy, tôi thường khuyên bạn nên đưa ra bổ đề của bạn với chiều dài của danh sách, chứ không phải trong danh sách. Sau đó bạn có thể chuyên nó. Đó sẽ là một cái gì đó như:

Lemma rev_eq_pal_length: forall (X: Type) (n: nat) (l: list X), length l <= n -> l = rev l -> pal l. 
Proof. 
(* by induction on [n], not [l] *) 
Qed. 

Theorem rev_eq_pal: forall (X: Type) (l: list X), l = rev l -> pal l. 
Proof. 
(* apply the previous lemma with n = length l *) 
Qed. 

Tôi có thể giúp bạn chi tiết hơn nếu cần, chỉ để lại nhận xét.

Chúc may mắn!

V.

EDIT: chỉ cần giúp bạn, tôi cần các bằng chứng sau đây để làm bằng chứng này, bạn cũng có thể cần chúng.

Lemma tool : forall (X:Type) (l l': list X) (a b: X),                           
      a :: l = l' ++ b :: nil -> (a = b /\ l = nil) \/ exists k, l = k ++ b :: nil. 

Lemma tool2 : forall (X:Type) (l1 l2 : list X) (a b: X),                           
    l1 ++ a :: nil = l2 ++ b :: nil -> a = b /\ l1 = l2. 

Answer 2

Bạn cũng có thể lấy nguyên tắc cảm ứng của mình từ một hình thức cảm ứng tốt.

Notation " [ ] " := nil : list_scope. 
Notation " [ x1 ; .. ; x2 ] " := (cons x1 .. (cons x2 nil) ..) : list_scope. 
Open Scope list_scope. 

Conjecture C1 : forall t1 f1 p1, (forall x1, (forall x2, f1 x2 < f1 x1 -> p1 x2) -> p1 x1) -> forall x1 : t1, p1 x1. 
Conjecture C2 : forall t1 p1, p1 [] -> (forall x1 l1, p1 ([x1] ++ l1)) -> forall l1 : list t1, p1 l1. 
Conjecture C3 : forall t1 p1, p1 [] -> (forall x1 l1, p1 (l1 ++ [x1])) -> forall l1 : list t1, p1 l1. 
Conjecture C4 : forall t1 (x1 x2 : t1) l1, length l1 < length ([x1] ++ l1 ++ [x2]). 

Theorem T1 : forall t1 p1, 
    p1 [] -> 
    (forall x1, p1 [x1]) -> 
    (forall x1 x2 l1, p1 l1 -> p1 ([x1] ++ l1 ++ [x2])) -> 
    forall l1 : list t1, p1 l1. 
Proof. 
intros t1 p1 h1 h2 h3. 
induction l1 as [l1 h4] using (C1 (list t1) (@length t1)). 
induction l1 as [| x1 l1] using C2. 
eapply h1. 
induction l1 as [| x2 l1] using C3. 
simpl. 
eapply h2. 
eapply h3. 
eapply h4. 
eapply C4. 
Qed. 

Bạn có thể chứng minh giả thuyết C1 bằng cách đầu tiên áp dụng các giả thuyết đến kết luận, sau đó sử dụng cảm ứng cấu trúc trên f1 x1, và sau đó sử dụng một số sự thật về <.

Để chứng minh C3, mà không có giả thuyết cảm ứng, trước tiên bạn phân tích trường hợp sử dụng trên is_empty l1, và sau đó sử dụng các sự kiện is_empty l1 = true -> l1 = [] và is_empty l1 = false -> l1 = delete_last l1 ++ [get_last l1] (get_last sẽ cần một giá trị mặc định).