Доказательство st X + st Y = st Y + (st X - 1) + 1 с использованием Coq

Question

Как и в названии, я ищу способ доказать st X + st Y = st Y + (st X - 1) + 1 в Coq. Я пробовал применять различные комбинации plus_comm, plus_assoc и plus_permute, но я не смог его пропустить. Какие-либо предложения?

Вот окно цели:

3 subgoal 
n : nat 
m : nat 
st : state 
H : st Y + st X = n + m /\ beval st (BNot (BEq (AId X) (ANum 0))) = true 
______________________________________(1/3) 
st Y + 1 + (st X - 1) = n + m 

Answer 1

Для целых чисел, либо ring или omega должен быть в состоянии решить такую ​​задачу. Это также можно сделать вручную. Это помогает отключить обозначения, чтобы отображались имена функций (для того, чтобы найти полезные лемм, используйте SearchAbout). Ниже, вероятно, не самое короткое доказательство, только первый я нашел:

Require Import ZArith. 

Lemma simple: forall x y, (x + y)%Z = (y + (x - 1) + 1)%Z. 
intros. 
rewrite Z.add_sub_assoc. 
replace ((y + x)%Z) with ((x + y)%Z). 
Focus 2. 
rewrite Z.add_comm. 
reflexivity. 
set (t := ((x + y)%Z)). 
replace (1%Z) with (Z.succ 0). 
Focus 2. 
symmetry. 
apply Z.one_succ. 
rewrite Zminus_succ_r. 
rewrite Z.add_succ_r. 
rewrite <- Zminus_0_l_reverse. 
rewrite <- Zplus_0_r_reverse. 
rewrite Z.succ_pred. 
reflexivity. 
Qed. 

Answer 2

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

inversion H. inversion H1. rewrite negb_true_iff in H3. apply beq_nat_false in H3. omega.

для почему омега работает после того, как мы делаем это и не тогда, когда цель была в первоначальном состоянии, здесь большой ответ на Github пользователя jaewooklee93:

«Вам не нужно подумайте о плюсе или компромиссе e, потому что омега может решить эти легкие проблемы. Ваши цели почти тривиальны, но причина, по которой омега не позволяет очистить цели, - это только то, что минус между nat не совпадает с тем, который мы уже знаем; 2-5 = 0, так как в nat нет понятия отрицательного. Поэтому, если вы не указали тот факт, что st X больше нуля, omega не может очистить цель для вас. Но у вас уже есть это условие в H1. Поэтому единственное, что вам нужно сделать, это упростить H1 и применить леммы к H1, чтобы сделать его st X <> 0. Тогда omega может нормально работать ».