CODEWITHSUNDEEP
coq
dimorphus
dimorphus

Reputation: 173

Coq: how to apply hypothesis with internal "if" branch

I need to apply FixL_Accumulate to prove the goal, but the unification fails due to the let statements and internal "if-then-else". The question is about how to match the shapes here?

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.

Upvotes: 0

Views: 93

Answers (1)

dimorphus
dimorphus

Reputation: 173

I've found the solution. The issue was because of the symmetry. Thus the question was incorrect.

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

Upvotes: 1

Related Questions