Доказательство равенства приложений в coq

Question

У меня есть последовательность приложений таким образом (f (f (fx))), являющаяся произвольной функцией f и любыми последовательностями номеров приложений.Я хочу доказать, что f (xy) и (x (fy)), x = (fff ...) и y = любое значение, оно равно.Мне нужно это доказательство в коде ниже:

Fixpoint r_nat {A : Type} (a : nat) : A -> (A -> A) -> A :=
  match a with
    |S n => fun (x0 : A) (a0 : A -> A) => r_nat n (a0 x0) a0
    |0 => fun (x0 : A) (_ : A -> A) => x0
  end. 


Theorem homomo_nat : forall {T} (f : T -> T) (h : T) (x : nat), (r_nat x (f h) f) = f ((r_nat x) h f) .
compute.
??.
Qed. 

Я пытаюсь развернуть и уточнить, но не работает.

Answer 1

Я переместил аргумент (x:nat) перед (h:T).Это делает гипотезу индукции сильнее - она ​​справедлива для all h.Тогда доказательство просто:

Theorem homomo_nat : forall {T} (f : T -> T) (x:nat) (h : T), (r_nat x (f h) f) = f ((r_nat x) h f) .
Proof.
  induction x.
  reflexivity.
  intros. apply IHx.
Qed.

Вы также можете «переместить аргументы» с помощью тактики, чтобы сохранить исходную теорему, если вы предпочитаете это ... Начните с intros; generalize dependent h.

Answer 2

Это должно быть решено индукцией на x, количество раз f применяется.