Skip to content

Instantly share code, notes, and snippets.

@anton-trunov

anton-trunov/tuple_rev_involutive.v

Created March 28, 2018 10:40
Show Gist options
  • Save anton-trunov/1c82bdb3b77a3488b1cd909328631e05 to your computer and use it in GitHub Desktop.
Save anton-trunov/1c82bdb3b77a3488b1cd909328631e05 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
tuple_rev_involutive.v
From Coq Require Import ssreflect ssrfun ssrbool.
From mathcomp Require Import eqtype seq tuple.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Definition trev T n (t : n.-tuple T) := [tuple of rev t].
Lemma trevK T n : involutive (@trev T n).
Proof. by move=>t; apply: val_inj; rewrite /= revK. Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment