Skip to content

Instantly share code, notes, and snippets.

@mukeshtiwari

mukeshtiwari/All_pairs.v

Created September 2, 2016 00:50
Show Gist options
  • Save mukeshtiwari/290b0eefd8064adda65d87845dede869 to your computer and use it in GitHub Desktop.
Save mukeshtiwari/290b0eefd8064adda65d87845dede869 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
All_pairs.v
(* all pairs that can be formed from a list *)
Fixpoint all_pairs {A: Type} (l: list A): list (A * A) :=
match l with
| [] => []
| c::cs => (c, c)::(all_pairs cs) ++ (map (fun x => (c, x)) cs)
++ (map (fun x => (x, c)) cs)
end.
A : Type
n : nat
l : list A
H1 : forall a : A, In a l
H2 : length l <= n
============================
(forall a : A * A, In a (all_pairs l)) /\ length (all_pairs l) <= n * n
@mukeshtiwari
Copy link
Author

Now
split. clear H2.
intros (a1, a2). induction l.
specialize (H1 a1). inversion H1.
simpl.

is leading towards more messier goal.

A : Type
n : nat
a : A
l : list A
H1 : forall a0 : A, In a0 (a :: l)
a1, a2 : A
IHl : (forall a : A, In a l) -> In (a1, a2) (all_pairs l)

(a, a) = (a1, a2) /
In (a1, a2) (all_pairs l ++ map (fun x : A => (a, x)) l ++ map (fun x : A => (x, a)) l)

subgoal 2 (ID 186) is:
length (all_pairs l) <= n * n

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment