Блог

Мне нужно применить FixL_Accumulate для доказательства цели, но объединение не удается из-за операторов let и внутреннего «if-then-else». Вопрос в том, как сопоставить формы здесь?

 Require Import ZArith.

Inductive branch (A B C : Prop) : Prop :=
  | Then: A -> B -> branch A B C
  | Else: not A -> C -> branch A B C
.

Definition itep (A B C : Prop) := (A -> B) / (~A -> C).
Axiom ite_then : forall A B C : Prop, itep A B C -> A -> B.
Axiom ite_else : forall A B C : Prop, itep A B C -> ~A -> C.
Axiom ite_both : forall A B C : Prop, itep A B C -> (B / C).
Axiom contrap: forall P Q : Prop, (P -> Q) -> ~Q -> ~P.

Parameter L_Accumulate : Z -> Z -> Z.
Hypothesis FixL_Accumulate: forall (n c: Z),
  let x := ((L_Accumulate n c))%Z in
  let x_1 := (n - 1%Z)%Z in itep ((n <= 0)%Z) ((x = c)%Z)
  (((n   ((L_Accumulate x_1 c%Z))) = x)%Z).

Goal
  forall (i c : Z),
  (i > 0)%Z ->
  ((((L_Accumulate i%Z c%Z)) = ((i   ((L_Accumulate (i - 1%Z)%Z c%Z))))%Z)).
Proof.
intros.
(* something like: apply (@FixL_Accumulate i c). *)
Qed.
  

Я нашел решение. Проблема заключалась в симметрии. Таким образом, вопрос был некорректным.

 Proof.
  intros.
  symmetry.
  apply (@FixL_Accumulate i c).
  intuition.
Qed.