Commit 2573a405 by Jean-Christophe Filliâtre

lemmas about permut and append moved to list.why

parent 8eb3ee63
 ... ... @@ -9,22 +9,6 @@ module M use import list.Append use import list.Permut lemma Permut_cons_append: forall x : 'a, l1 l2 : list 'a. permut (Cons x l1 ++ l2) (l1 ++ Cons x l2) lemma Permut_assoc: forall l1 l2 l3: list 'a. permut ((l1 ++ l2) ++ l3) (l1 ++ (l2 ++ l3)) lemma Permut_append: forall l1 l2 k1 k2 : list 'a. permut l1 k1 -> permut l2 k2 -> permut (l1 ++ l2) (k1 ++ k2) lemma Permut_append_swap: forall l1 l2 : list 'a. permut (l1 ++ l2) (l2 ++ l1) let split l0 = { length l0 >= 2 } let rec split_aux (l1 : list 'a) l2 l variant { length l } = ... ...
This diff is collapsed.
 ... ... @@ -211,6 +211,24 @@ theory Permut lemma Permut_swap: forall x y: 'a, l: list 'a. permut (Cons x (Cons y l)) (Cons y (Cons x l)) use import Append lemma Permut_cons_append: forall x : 'a, l1 l2 : list 'a. permut (Cons x l1 ++ l2) (l1 ++ Cons x l2) lemma Permut_assoc: forall l1 l2 l3: list 'a. permut ((l1 ++ l2) ++ l3) (l1 ++ (l2 ++ l3)) lemma Permut_append: forall l1 l2 k1 k2 : list 'a. permut l1 k1 -> permut l2 k2 -> permut (l1 ++ l2) (k1 ++ k2) lemma Permut_append_swap: forall l1 l2 : list 'a. permut (l1 ++ l2) (l2 ++ l1) use import Mem lemma Permut_mem: ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!