Skip to content

Instantly share code, notes, and snippets.

@mukeshtiwari

mukeshtiwari/Fail.v

Created August 23, 2024 17:12
Show Gist options
  • Save mukeshtiwari/c1b0d59c6bd3dca7e91840c0a3b4be07 to your computer and use it in GitHub Desktop.
Save mukeshtiwari/c1b0d59c6bd3dca7e91840c0a3b4be07 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Fail.v
From Coq Require Import
Program.Tactics
List Psatz.
Definition nth_safe {A : Type}
(l : list A) (n : nat) (Ha : (n < length l)) : A.
Proof.
refine
(match (nth_error l n) as nth return (nth_error l n) = nth -> A with
| Some res => fun Hb => res
| None => fun Hb => _
end eq_refl).
eapply nth_error_None in Hb;
abstract nia.
Defined.
(*
Next Obligation.
symmetry in Heq_anonymous. apply nth_error_None in Heq_anonymous. lia.
Defined.
*)
Lemma nth_safe_nth: forall
{A : Type} (l : list A) (n : nat) d
(Ha : (n < length l)), nth_safe l n Ha = nth n l d.
Proof.
intros *. unfold nth_safe.
Fail destruct (nth_error l n).
pose (fn := (fun (la : list A) (na : nat) (Hb : na < length la)
(o : option A) (Hc : nth_error la na = o) =>
match o as nth return nth_error la na = nth -> A with
| Some res => fun _ : nth_error la na = Some res => res
| None => fun Hbt : nth_error la na = None =>
nth_safe_subproof A la na Hb
(match nth_error_None la na with
| conj H _ => H
end Hbt)
end Hc) l n Ha).
enough (forall (o : option A) Ht, fn o Ht = nth n l d) as Htt.
+
eapply Htt.
+
intros *.
destruct o as [x |].
++
simpl. eapply eq_sym, nth_error_nth.
exact Ht.
++
pose proof (proj1(nth_error_None l n) Ht).
nia.
Qed.
@mukeshtiwari
Copy link
Author

A : Type
l : list A
n : nat
d : A
Ha : n < length l

match nth_error l n as nth return (nth_error l n = nth -> A) with
| Some res => fun _ : nth_error l n = Some res => res
| None =>
fun Hb : nth_error l n = None =>
nth_safe_subproof A l n Ha (match nth_error_None l n with
| conj H _ => H
end Hb)
end eq_refl = nth n l d

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