(* week-12_induction-and-coinduction-for-reasoning-about-streams.v *) (* LPP 2025 - CS3234 2024-2025, Sem2 *) (* Olivier Danvy *) (* Version of 10 Apr 2025 *) (* ********** *) Require Import Arith Bool List. (* ********** *) (* Paraphernalia for reasoning equationally: *) Ltac fold_unfold_tactic name := intros; unfold name; fold name; reflexivity. (* ********** *) (* Polymorphic streams: *) CoInductive stream (V : Type) : Type := SCons : V -> stream V -> stream V. (* ********** *) (* "stream_index V n vs" maps the stream vs into its element at index n *) Fixpoint stream_index (V : Type) (vs : stream V) (n : nat) : V := match n with 0 => match vs with SCons _ v _ => v end | S n' => match vs with SCons _ _ vs' => stream_index V vs' n' end end. Lemma fold_unfold_stream_index_O : forall (V : Type) (vs : stream V), stream_index V vs 0 = match vs with SCons _ v _ => v end. Proof. fold_unfold_tactic stream_index. Qed. Lemma fold_unfold_stream_index_S : forall (V : Type) (vs : stream V) (n' : nat), stream_index V vs (S n') = match vs with SCons _ _ vs' => stream_index V vs' n' end. Proof. fold_unfold_tactic stream_index. Qed. (* ********** *) (* Bisimilarity -- the coinductive counterpart of structural equality: *) CoInductive bisimilar : forall V : Type, (V -> V -> bool) -> stream V -> stream V -> Prop := Bisimilar : forall (V : Type) (eqb_V : V -> V -> bool) (v1 v2 : V), eqb_V v1 v2 = true -> (* 1 *) forall v1s v2s : stream V, bisimilar V eqb_V v1s v2s -> (* 2 *) bisimilar V eqb_V (SCons V v1 v1s) (SCons V v2 v2s). (* 3 *) (* ********** *) (* A variety of properties about bisimilarity: *) Property Bisimilar_12_3 : (* 1 -> 2 -> 3 *) forall (V : Type) (eqb_V : V -> V -> bool) (v1 v2 : V) (v1s v2s : stream V), eqb_V v1 v2 = true -> (* 1 *) bisimilar V eqb_V v1s v2s -> (* 2 *) bisimilar V eqb_V (SCons V v1 v1s) (SCons V v2 v2s). (* 3 *) Proof. intros V eqb_V v1 v2 v1s v2s eqb_v1_v2. revert V eqb_V v1 v2 eqb_v1_v2 v1s v2s. exact Bisimilar. Qed. Property Bisimilar_3_12 : (* 3 -> 1 /\ 2 *) forall (V : Type) (eqb_V : V -> V -> bool) (v1 v2 : V) (v1s' v2s' : stream V), bisimilar V eqb_V (SCons V v1 v1s') (SCons V v2 v2s') -> (* 3 *) eqb_V v1 v2 = true /\ bisimilar V eqb_V v1s' v2s'. (* 1 /\ 2 *) Proof. intros V eqb_V v1 v2 v1s' v2s' bs_v1s'_v2s'. remember (SCons V v1 v1s') as v1s eqn:H_v1s. remember (SCons V v2 v2s') as v2s eqn:H_v2s. case bs_v1s'_v2s' as [V' eqb_V' v1' v2' eq_v1'_v2' v1s'' v2s'' bs_v1s''_v2s'']. injection H_v1s as eq_v1'_v1 eq_v1s''_v1s'. injection H_v2s as eq_v2'_v2 eq_v2s''_v2s'. rewrite <- eq_v1'_v1. rewrite <- eq_v2'_v2. rewrite <- eq_v1s''_v1s'. rewrite <- eq_v2s''_v2s'. exact (conj eq_v1'_v2' bs_v1s''_v2s''). Qed. Property Bisimilar_13_2 : (* 1 -> 3 -> 2 *) forall (V : Type) (eqb_V : V -> V -> bool) (v1 v2 : V) (v1s v2s : stream V), eqb_V v1 v2 = true -> (* 1 *) bisimilar V eqb_V (SCons V v1 v1s) (SCons V v2 v2s) -> (* 3 *) bisimilar V eqb_V v1s v2s. (* 2 *) Proof. intros V eqb_V v1 v2 v1s v2s eqb_v1_v2 bs_v1_v1s_v2_v2s. remember (SCons V v1 v1s) as v1s' eqn:H_v1s'. remember (SCons V v2 v2s) as v2s' eqn:H_v2s'. case bs_v1_v1s_v2_v2s as [V' eqb_V' v1' v2' eqb_v1'_v2' v1s'' v2s'' bs_v1s''_v2s'']. injection H_v1s' as eq_v1'_v1 eq_v1s''_v1s. injection H_v2s' as eq_v2'_v2 eq_v2s''_v2s. rewrite <- eq_v1s''_v1s. rewrite <- eq_v2s''_v2s. exact bs_v1s''_v2s''. Qed. Property Bisimilar_23_1 : (* 2 -> 3 -> 1 *) forall (V : Type) (eqb_V : V -> V -> bool) (v1 v2 : V) (v1s v2s : stream V), bisimilar V eqb_V v1s v2s -> (* 2 *) bisimilar V eqb_V (SCons V v1 v1s) (SCons V v2 v2s) -> (* 3 *) eqb_V v1 v2 = true. (* 1 *) Proof. intros V eqb_V v1 v2 v1s v2s bs_v1s_v2s_v2 bs_v1_v1s_v2_v2s. remember (SCons V v1 v1s) as v1s' eqn:H_v1s'. remember (SCons V v2 v2s) as v2s' eqn:H_v2s'. case bs_v1_v1s_v2_v2s as [V' eq_V' v1' v2' eqb_v1'_v2' v1s'' v2s'' bs_v1s''_v2s'']. injection H_v1s' as eq_v1'_v1 eq_v1s''_v1s. injection H_v2s' as eq_v2'_v2 eq_v2s''_v2s. rewrite <- eq_v1'_v1. rewrite <- eq_v2'_v2. exact eqb_v1'_v2'. Qed. (* ********** *) (* Bisimilarity is an equivalence relation: *) Proposition bisimilar_refl : forall (V : Type) (eqb_V : V -> V -> bool), (forall v : V, eqb_V v v = true) -> forall vs : stream V, bisimilar V eqb_V vs vs. Proof. intros V eqb_V eqb_V_refl. cofix coIH. intros [v vs']. Check (Bisimilar V eqb_V v v (eqb_V_refl v) vs' vs' (coIH vs')). exact (Bisimilar V eqb_V v v (eqb_V_refl v) vs' vs' (coIH vs')). Qed. Proposition bisimilar_sym : forall (V : Type) (eqb_V : V -> V -> bool), (forall v1 v2 : V, eqb_V v1 v2 = true -> eqb_V v2 v1 = true) -> forall v1s v2s : stream V, bisimilar V eqb_V v1s v2s -> bisimilar V eqb_V v2s v1s. Proof. intros V eqb_V eqb_V_sym. cofix coIH. intros [v1 v1s'] [v2 v2s'] bs_v1s_v2s. Check (Bisimilar_3_12 V eqb_V v1 v2 v1s' v2s' bs_v1s_v2s). destruct (Bisimilar_3_12 V eqb_V v1 v2 v1s' v2s' bs_v1s_v2s) as [eq_v1_v2 bs_v1s'_v2s']. Check (Bisimilar V eqb_V v2 v1 (eqb_V_sym v1 v2 eq_v1_v2)). Check (Bisimilar V eqb_V v2 v1 (eqb_V_sym v1 v2 eq_v1_v2) v2s' v1s'). Check (Bisimilar V eqb_V v2 v1 (eqb_V_sym v1 v2 eq_v1_v2) v2s' v1s' (coIH v1s' v2s' bs_v1s'_v2s')). exact (Bisimilar V eqb_V v2 v1 (eqb_V_sym v1 v2 eq_v1_v2) v2s' v1s' (coIH v1s' v2s' bs_v1s'_v2s')). Qed. Proposition bisimilar_trans : forall (V : Type) (eqb_V : V -> V -> bool), (forall v1 v2 v3: V, eqb_V v1 v2 = true -> eqb_V v2 v3 = true -> eqb_V v1 v3 = true) -> forall v1s v2s v3s: stream V, bisimilar V eqb_V v1s v2s -> bisimilar V eqb_V v2s v3s -> bisimilar V eqb_V v1s v3s. Proof. Admitted. (* ********** *) Theorem bisimilarity_implies_indexing : forall (V : Type) (eqb_V : V -> V -> bool) (v1s v2s : stream V), bisimilar V eqb_V v1s v2s -> forall n : nat, eqb_V (stream_index V v1s n) (stream_index V v2s n) = true. Proof. intros V eqb_V v1s v2s bs_v1s_v2s n. revert v1s v2s bs_v1s_v2s. induction n as [ | n' IHn']; intros [v1 v1s'] [v2 v2s'] bs_v1s_v2s. - rewrite ->2 fold_unfold_stream_index_O. destruct (Bisimilar_3_12 V eqb_V v1 v2 v1s' v2s' bs_v1s_v2s) as [eqb_v1_v2 bs_v1s'_v2s']. exact eqb_v1_v2. - rewrite ->2 fold_unfold_stream_index_S. destruct (Bisimilar_3_12 V eqb_V v1 v2 v1s' v2s' bs_v1s_v2s) as [eqb_v1_v2 bs_v1s'_v2s']. exact (IHn' v1s' v2s' bs_v1s'_v2s'). Qed. Theorem indexing_implies_bisimilarity : forall (V : Type) (eqb_V : V -> V -> bool) (v1s v2s : stream V), (forall n : nat, eqb_V (stream_index V v1s n) (stream_index V v2s n) = true) -> bisimilar V eqb_V v1s v2s. Proof. intros V eqb_V. cofix coIH. intros [v1 v1s'] [v2 v2s'] H_index. assert (H_index_0 := H_index 0). rewrite ->2 fold_unfold_stream_index_O in H_index_0. Check (Bisimilar V eqb_V v1 v2 H_index_0 v1s' v2s'). apply (Bisimilar V eqb_V v1 v2 H_index_0 v1s' v2s'). Check (coIH v1s' v2s'). apply (coIH v1s' v2s'). intro n. assert (H_index_Sn := H_index (S n)). rewrite ->2 fold_unfold_stream_index_S in H_index_Sn. exact H_index_Sn. Qed. Theorem equivalence_of_bisimilarity_and_indexing : forall (V : Type) (eqb_V : V -> V -> bool) (v1s v2s : stream V), (forall n : nat, eqb_V (stream_index V v1s n) (stream_index V v2s n) = true) <-> bisimilar V eqb_V v1s v2s. Proof. intros V eqb_V v1s v2s. split. - exact (indexing_implies_bisimilarity V eqb_V v1s v2s). - exact (bisimilarity_implies_indexing V eqb_V v1s v2s). Qed. (* ********** *) (* week-12_induction-and-coinduction-for-reasoning-about-streams.v *)