[coq] safe head of list
This commit is contained in:
parent
09ede3acde
commit
e7d8161acb
|
@ -0,0 +1,35 @@
|
|||
Require Import List.
|
||||
Import ListNotations.
|
||||
|
||||
Section Foo.
|
||||
Context {A:Type}.
|
||||
|
||||
Definition hdpf (l:list A) (pf: l <> []): A :=
|
||||
(match l return l <> [] -> A with
|
||||
| [] => fun pf' => match pf' eq_refl with end
|
||||
| x::_ => fun _ => x
|
||||
end) pf.
|
||||
End Foo.
|
||||
|
||||
Ltac tacNotNil l := unfold l; intros H; inversion H.
|
||||
|
||||
Example l1 := [1;2;3].
|
||||
|
||||
Lemma l1NotNil: l1 <> [].
|
||||
Proof. tacNotNil l1. Qed.
|
||||
|
||||
Compute hdpf [1;2;3] (ltac:(tacNotNil l1)).
|
||||
(* = 1 : nat *)
|
||||
|
||||
Compute
|
||||
let l := [1] in
|
||||
hdpf l (ltac:(tacNotNil l)).
|
||||
|
||||
Compute
|
||||
let l := [true; false] in
|
||||
hdpf l (ltac:(tacNotNil l)).
|
||||
|
||||
Compute
|
||||
let l := [] in
|
||||
hdpf l (ltac:(tacNotNil l)).
|
||||
(* I wonder why this didn't give an outright error... *)
|
Loading…
Reference in New Issue