Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
(* http://stackoverflow.com/questions/43849824/coq-rewriting-using-lambda-arguments/ *)
Require Import Coq.Lists.List. Import ListNotations.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Setoids.Setoid.
Require Import Coq.Classes.Morphisms.
Generalizable All Variables.
Instance subrel_eq_respect {A B : Type} `(sa : subrelation A RA eq)
`(sb : subrelation B eq RB) :
subrelation eq (respectful RA RB).
Proof. intros. intros f g Hfg. subst. intros a a' Raa'. apply sb.
f_equal. apply (sa _ _ Raa'). Qed.
Instance pointwise_eq_ext {A B : Type} `(sb : subrelation B RB eq)
: subrelation (pointwise_relation A RB) eq.
Proof. intros f g Hfg. apply functional_extensionality. intro x; apply sb, (Hfg x). Qed.
Fixpoint inject_into {A} (x : A) (l : list A) (n : nat) : option (list A) :=
match n, l with
| 0, _ => Some (x :: l)
| S k, [] => None
| S k, h :: t => let kwa := inject_into x t k
in match kwa with
| None => None
| Some l' => Some (h :: l')
end
end.
Theorem inject_correct_index : forall A x (l : list A) n,
n <= length l -> exists l', inject_into x l n = Some l'.
Admitted.
Variable iota : nat -> list nat. (* no implementation *)
Fixpoint permute {A} (l : list A) : list (list A) :=
match l with
| [] => [[]]
| h :: t => flat_map (
fun x => map (
fun y => match inject_into h x y with
| None => []
| Some permutations => permutations
end
) (iota (length t))) (permute t)
end.
Variable factorial : nat -> nat. (* no implementation *)
Theorem num_permutations : forall A (l : list A) k,
length l = k -> length (permute l) = factorial k.
Proof.
induction l.
- admit.
- cbn; intros.
(* the first version of the question stated explicitly the following *)
assert (forall x y, inject_into a x y = Some x) as Hr. { admit. }
setoid_rewrite Hr.
Admitted.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment