Skip to content

Instantly share code, notes, and snippets.

@yoshihiro503

yoshihiro503/長さ付きリストの証明_ssreflect.v

Created July 12, 2024 06:42
Show Gist options
  • Save yoshihiro503/b9bc446e0f5e0290ce442ee649a4d97c to your computer and use it in GitHub Desktop.
Save yoshihiro503/b9bc446e0f5e0290ce442ee649a4d97c to your computer and use it in GitHub Desktop.
Download ZIP
Raw
長さ付きリストの証明_ssreflect.v
From mathcomp Require Import all_ssreflect.
Require Import JMeq.
Inductive sizseq (T:Type) : nat -> Type :=
| SizNil : sizseq T 0
| SizCons n : T -> sizseq T n -> sizseq T n.+1.
Lemma sizseq0nil_aux (T:Type) n : forall xs : sizseq T n, n = 0 -> JMeq xs (SizNil T).
Proof.
move=> xs. now case_eq xs.
Qed.
Lemma sizseq0nil (T:Type) : all_equal_to (@SizNil T).
Proof.
move=> xs. exact/JMeq_eq/sizseq0nil_aux.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment