(* CoInductive stream (A : Type) : Type := | Cons : A -> stream A -> stream A. CoFixpoint zeroes : stream nat := Cons nat 0 zeroes. *) (*Print Fix. Print Fix_F. *) (* Fixpoint bad (n : nat) : nat := match n with | O => 0 | S n => bad (S (S n)) end. *) Fixpoint F (n : nat) : nat := (fun _=> O)(F n). Fixpoint F2 (n : nat ) : nat := match n with | O => O | S x => (fun z => O) (F (S x)) end. (* This is an example above showing that Coq is not SN. https://pastel.archives-ouvertes.fr/file/index/docid/622429/filename/21076_SACCHINI_2011_archivage.pdf sect 1.2.1 *) (* https://sympa.inria.fr/sympa/arc/coq-club/2016-02/msg00248.html *) CoInductive inftree := | node : nat -> inftree -> inftree -> inftree. CoFixpoint one : inftree := node 1 one one. CoFixpoint zero : inftree := node 0 zero zero. CoFixpoint il : inftree := node 0 il' il' with il' : inftree := node 1 il il. CoFixpoint il'' : inftree := node 0 (node 1 il'' il'') (node 1 il'' il''). CoFixpoint interleave (a : inftree) (b : inftree) : inftree := match a with node x a1 a2 => node x (interleave b a1) (interleave b a2) end. CoFixpoint interleave' (a : inftree) (b : inftree) : inftree := match a with node x a1 a2 => match b with node y b1 b2 => node x (node y (interleave a1 b1) (interleave a1 b2)) (node y (interleave a2 b1) (interleave a2 b2)) end end. Inductive tree := | emptytree | Node : nat -> tree -> tree -> tree. Fixpoint approx (a : inftree) (n : nat) := match n with | 0 => emptytree | S n' => match a with node x a1 a2 => Node x (approx a1 n') (approx a2 n') end end. Eval simpl in approx il 4. Eval simpl in approx il'' 4. Eval simpl in approx (interleave one zero) 4. Eval simpl in il. Fixpoint good (a : tree) : tree := match a with | emptytree => emptytree | Node x a1 a2 => Node x (good a2) (good a1) end. CoFixpoint good' (a : inftree) : inftree := match a with | node x a1 a2 => node x (good' a2) (good' a1) end. Fixpoint still_good (a : tree) : tree := match a with | emptytree => emptytree | Node x a1 a2 => good a2 end. (* CoFixpoint not_so_good' (a : inftree) : inftree := match a with | node x a1 a2 => not_so_good' a2 end. *) (* CoFixpoint bad (a : inftree) : inftree := match a with | node x a1 a2 => good' (node x a2 a1) end. *) CoFixpoint strange (a : inftree) : inftree := match a with | node x a1 a2 => (fun f => zero) (strange a2) end. (* the last example shows that beta-reduction is performed before guardedness checks... *) (*** equivalence ***) Definition lft (a : inftree) := match a with node _ l _ => l end. Definition rt (a : inftree) := match a with node _ _ r => r end. Definition head (a : inftree) := match a with node x _ _ => x end. CoInductive tree_eq (a : inftree) (b : inftree) : Prop := | treq : head a = head b -> (tree_eq (lft a) (lft b)) -> (tree_eq (rt a) (rt b)) -> tree_eq a b. (* cf.: CoInductive inftree := | node : nat -> inftree -> inftree -> inftree. *) Eval simpl in (approx il 4). Eval simpl in (approx (interleave zero one) 4). Lemma unfold_tree : forall a : inftree, a = match a with node x a1 a2 => node x a1 a2 end. Proof. intros. destruct a. reflexivity. Qed. Lemma ile : tree_eq il (interleave zero one). Proof. cofix CIH. rewrite (unfold_tree il). rewrite (unfold_tree (interleave zero one)). simpl. apply treq. simpl. reflexivity. simpl. rewrite (unfold_tree il'). rewrite (unfold_tree (interleave one zero)). simpl. apply treq. simpl. reflexivity. simpl. assumption. simpl. assumption. (* the same for the other branch *) rewrite (unfold_tree il'). rewrite (unfold_tree (interleave one zero)). simpl. apply treq. simpl. reflexivity. simpl. assumption. simpl. assumption. Qed. Print ile. (* could use 'constructor' tactic instead of 'apply treq' *)