Объединить дубликаты в матче Coq

Question

Я много раз сталкивался с этой проблемой: у меня есть доказательство в Coq, которое включает совпадения по обе стороны от равенства, которые являются одинаковыми.

Есть ли стандартный способ переписать несколько совпадений в один?

Например.

match expression_evaling_to_Z with 
    Zarith.Z0 => something 
    Zartih.Pos _ => something_else 
    Zarith.Neg _ => something_else 
end = yet_another_thing. 

И если я уничтожить на expresion_evaling_to_Z я получаю две одинаковые цели. Я хотел бы найти способ получить только одну из целей.

Answer 1

Стандартное решение состоит в том, чтобы определить «представление» вашего типа данных с использованием семейства типов, которое представит правильные условия и случаи, когда они будут разрушены. Для вашего конкретного случая, вы могли бы сделать:

Require Import Coq.ZArith.ZArith. 

Inductive zero_view_spec : Z -> Type := 
| Z_zero :      zero_view_spec Z0 
| Z_zeroN : forall z, z <> Z0 -> zero_view_spec z. 

Lemma zero_viewP z : zero_view_spec z. 
Proof. now destruct z; [constructor|constructor 2|constructor 2]. Qed. 

Lemma U z : match z with 
       Z0    => 0 
      | Zpos _ | Zneg _ => 1 
      end = 0. 
Proof. 
destruct (zero_viewP z). 
Abort. 

Это общая идиома в некоторых библиотеках, как по математике-Comp, которая обеспечивает специальную поддержку для инстанцирования z аргумента семьи типа.

Answer 2

Вы можете написать выражение match более лаконично:

match expression_evaling_to_Z with 
    | Z0 => something 
    | Zpos _ | Zneg _ => something_else 
end = yet_another_thing. 

Но это даст вам 3 подцели при использовании destruct.

В этом конкретном случае мы можем использовать тот факт, что вам действительно нужно различать нулевые и ненулевые случаи, и это похоже на работу для функции Z.abs_nat : Z -> nat.

Require Import Coq.ZArith.BinIntDef. 

match Z.abs_nat (expression_evaling_to_Z) with 
    | O => something 
    | S _ => something_else 
end = yet_another_thing. 

Это поможет вам только два подслучая, но вам нужно уничтожить на Z.abs_nat (expression_evaling_to_Z) или ввести новую переменную. Если вы выберете 1-й вариант, вам, вероятно, понадобится destruct (...) eqn:Heq., чтобы привести уравнение в контекст.

В основном этот подход касается поиска нового типа данных (или определения его) и подходящей функции для сопоставления старого и нового типов.

Answer 3

Если вы не против печатать, вы можете использовать replace, чтобы заменить RHS на LHS вашей цели, что делает его тривиальным для решения, а затем вам просто нужно доказать, что переписывание действительно нормально.

Open Scope Z. 
Lemma L a b : 
    match a + b with 
     Z0  => a + b 
    | Zpos _ => b + a 
    | Zneg _ => b + a 
    end = a + b. 
    replace (b+a) with (a+b). (* 1. replace the RHS with something trivially true *) 
    destruct (a+b); auto.  (* 2. solve the branches in one fell swoop *) 
    apply Z.add_comm.   (* 3. solve only once what is required for the two brances *) 
Qed. 

Может быть, вы можете использовать некоторые Ltac-фу или другую лемму не должны вводить в RHS тоже вручную.