Làm thế nào để cấm chiến thuật đơn giản để mở ra các biểu thức số học?

Question

Chiến thuật simpl mở ra các biểu thức như 2 + a thành "cây phù hợp" không hề đơn giản chút nào. Ví dụ:

Goal forall i:Z, ((fun x => x + i) 3 = i + 3). 
simpl. 

Dẫn đến:

forall i : Z, 
match i with 
| 0 => 3 
| Z.pos y' => 
    Z.pos 
     match y' with 
     | q~1 => 
      match q with 
      | q0~1 => (Pos.succ q0)~1 
      | q0~0 => (Pos.succ q0)~0 
      | 1 => 3 
      end~0 
     | q~0 => 
      match q with 
      | q0~1 => (Pos.succ q0)~0 
      | q0~0 => q0~1 
      | 1 => 2 
      end~1 
     | 1 => 4 
     end 
| Z.neg y' => Z.pos_sub 3 y' 
end = i + 3 

Làm thế nào để tránh biến chứng như vậy với simpl chiến thuật?

Mục tiêu cụ thể này có thể được giải quyết với omega, nhưng nếu nó phức tạp hơn một chút, thì lỗi omega không thành công và tôi phải sử dụng thứ gì đó như: replace (2 + a) with (a + 2); simpl; replace (a + 2) with (2 + a).

Answer 1

Bạn có thể kiểm soát định nghĩa đang diễn ra với các lệnh Transparent và Opaque. Trong ví dụ của bạn, bạn sẽ có thể nói điều gì đó như

Opaque Z.add. 
simpl. 
Transparent Z.add. 

Ngoài ra, Argumentscommand có thể được sử dụng để chỉ thị cho simpl chiến thuật để tránh đơn giản hóa điều khoản trong bối cảnh nhất định. Ví dụ.

Arguments Z.add _ _ : simpl nomatch. 

thực hiện thủ thuật cho tôi trong trường hợp của bạn. Biến thể cụ thể này làm gì để tránh đơn giản hóa một thuật ngữ khi một số lớn, xấu xí match sẽ xuất hiện ở vị trí đầu sau khi thực hiện điều đó (những gì bạn đã thấy trong ví dụ của mình). Có những biến thể khác nữa, tuy nhiên.

Cuối cùng, chỉ để hoàn thành, thư viện Ssreflect cung cấp cơ sở hạ tầng tốt đẹp để làm cho một số định nghĩa mờ đục cục bộ. Vì vậy, bạn có thể nói cái gì đó như

rewrite (lock Z.add) /= -lock. 

có nghĩa là "khóa Z.add, do đó nó sẽ không đơn giản hóa, sau đó đơn giản hóa việc còn lại của biểu thức (các /= switch), sau đó mở khóa định nghĩa lại (-lock)".

Answer 2

Bạn có thể tinh chỉnh cách chiến thuật đơn giản hoạt động để bạn nhận được ít trận đấu hơn.

Đọc thêm về nó here.

Nếu không, bạn có thể sử dụng other tactics cho phép bạn chọn cách giảm. Ví dụ: cbn beta.