Saya telah membaca di sini bahwa pada daftar terbatas dimungkinkan untuk menulis foldR dalam istilah foldL dengan cara berikut ( menggunakan coq):

Fixpoint fold {A : Type} {B : Type} (f : A -> B -> B) (v : B) (l : list A) :=
  match l with
  | nil => v
  | x :: xs => f x (fold f v xs)
  end.

Fixpoint foldL {A : Type} {B : Type} (f : B -> A -> B) (v : B) (l : list A) :=
  match l with
  | nil => v
  | x :: xs => foldL f (f v x) xs
  end.

Definition fold' {A B : Type} (f : B -> A -> A) (a : A) (xs : list B) :=
  foldL (fun g b x => g (f b x)) id xs a.

Sekarang saya ingin menunjukkan bahwa fold dan fold' adalah sama:

Theorem fold_eq_fold' {A : Type} {B : Type} :
  forall
    (f : B -> A -> A) 
    (v : A),
      fold f v = fold' f v.
Proof.
  intros.
  unfold fold'.
  apply functional_extensionality.
  intros.
  induction x; intros; simpl in *.
  - trivial.
  - rewrite IHx. 
Abort.

Tapi saya tidak bisa menutup teorema ini.

Bisakah seseorang membantu saya?

Sunting

Berkat jawaban Meven Lennon-Bertrand, saya dapat menutup teorema:

Lemma app_cons {A: Type} :
  forall 
    (l1 : list A)
    (l2 : list A)
    (a : A),
      l1 ++ a :: l2 = (l1 ++ [a]) ++ l2.
Proof.
  intros.
  rewrite <- app_assoc. 
  trivial.
Qed.

Theorem fold_eq_fold' {A : Type} {B : Type} :
  forall
    (f : B -> A -> A) 
    (a : A)
    (l : list B),
      fold f a l = fold' f a l.
Proof.
  intros.
  unfold fold'.
  change id with (fun x => fold f x nil).
  change l with (nil ++ l) at 1.
  generalize (@nil B).
  induction l; intros; simpl.
  - rewrite app_nil_r. trivial.
  - rewrite app_cons. rewrite IHl. 
    assert((fun x : A => fold f x (l0 ++ [a0])) = (fun x : A => fold f (f a0 x) l0)).
    + apply functional_extensionality; intros.
      induction l0; simpl.
      * trivial.
      * rewrite IHl0. trivial.
    + rewrite H. trivial.
Qed.
0
Marco Mantovani 8 April 2021, 20:01

1 menjawab

Jawaban Terbaik

Masalahnya adalah dengan hipotesis induksi Anda: itu tidak cukup umum, karena ini berbicara tentang id, yang tidak ada gunanya dalam tujuan kedua Anda. Anda dapat membuatnya cukup umum dengan sesuatu seperti ini:

Theorem fold_eq_fold' {A : Type} {B : Type} :
  forall
    (f : B -> A -> A) 
    (a : A)
    (l : list B),
      fold f a l = fold' f a l.
Proof.
  intros.
  unfold fold'.
  change id with (fun x => fold f x nil).
  change l with (nil ++ l) at 1.
  generalize (@nil B).

Ini memberi Anda tujuan bentuk yang lebih umum, yang menjadikan Anda sebagai kasus khusus dengan nil. Sekarang yang satu ini seharusnya lebih mudah ditangani dengan induksi pada l.

1
Meven Lennon-Bertrand 9 April 2021, 09:47