đệ quy nghịch đảo các giả thuyết trong coq

Question

Tôi đang gặp khó khăn trong việc xác định chiến thuật để đảo ngược đệ quy giả thuyết trong ngữ cảnh chứng minh. Ví dụ, giả sử tôi có một bối cảnh chứng minh có chứa một giả thuyết như:

H1 : search_tree (node a (node b ll lr) (node c rl rr)) 

và muốn lặp đi lặp lại đảo ngược giả thuyết để có được một bối cảnh chứng minh có chứa các giả thuyết

H1 : search_tree (node a (node b ll lr) (node c rl rr)) 
H2 : search_tree (node b ll lr) 
H3 : search_tree (node c rl rr) 
H4 : lt_tree a (node b ll lr) 
H5 : gt_tree a (node c rl rr) 
H6 : lt_tree b ll 
H7 : gt_tree b lr 
H8 : lt_tree c rl 
H9 : gt_tree c rr 

Tất nhiên, việc thu thập bằng chứng này bối cảnh dễ dàng bằng cách áp dụng nhiều lần chiến thuật đảo ngược. Tuy nhiên, đôi khi đảo ngược một giả thuyết sẽ đưa các giả thuyết khác nhau vào các bản phụ khác nhau và liệu có đảo ngược từng phụ thuộc vào bản chất của thông tin được cung cấp bởi sự đảo ngược hay không.

Vấn đề hiển nhiên là việc kết hợp mẫu bừa bãi chống lại ngữ cảnh chứng minh sẽ gây ra không có kết quả. Ví dụ: những điều sau đây sẽ không hoạt động nếu một người muốn giữ lại các giả thuyết ban đầu sau khi đảo ngược chúng:

Ltac invert_all := 
    match goal with 
    | [ H1 : context [ node ?a ?l ?r ] |- ?goal ] => invert H1; invert_all 
    | _ => idtac 
    end. 

Có cách nào dễ dàng để làm điều này? Giải pháp rõ ràng là giữ một chồng các giả thuyết đảo ngược. Một giải pháp khác là chỉ đảo ngược các giả thuyết lên đến một độ sâu cụ thể, điều này sẽ loại bỏ các cuộc gọi đệ quy trong Ltac.

Answer 1

Nếu đó là thực sự những gì bạn muốn làm, tôi nghi ngờ bạn muốn đầu tiên để chứng minh một helper Fixpoint subtreelist (st : searchtree): list (...) mà trả về một danh sách của tất cả các subtrees, và sau đó một chiến thuật mà các cuộc gọi subtreelist và đệ quy destruct s danh sách cho đến khi bạn có tất cả các thêm giả thuyết bạn muốn.

Chúc may mắn với điều đó!