Skip to content

Instantly share code, notes, and snippets.

View ikanher's full-sized avatar

Aki Rehn ikanher

4 followers · 1 following
  • Helsinki
View GitHub Profile
@ikanher
ikanher / vi-exercise-gradient-2d-pyro.ipynb
Created January 26, 2022 18:04
Variational inference with Pyro
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
@ikanher
ikanher / gist:eebd05c77997c26101f3ec5455b2d681
Created July 6, 2018 14:25
Problem with conditional_2 proof...
Require Import Classical.
(*
¬(P ∧ Q) ⇔ (¬P ∨ ¬Q)
*)
Theorem demorgan_1: forall P Q : Prop, ~(P /\ Q) <-> (~P \/ ~Q).
Proof. intros p q. unfold iff. split.
- intros H. apply not_and_or in H. assumption.
- intros H. apply or_not_and in H. assumption. Qed.
@ikanher
ikanher / gist:f75eca7a6da9c5c02b0cd4190f9c9812
Created July 4, 2018 19:09
Beginning of How to Prove it proves in Coq.
Require Import Classical.
(*
¬(P ∧ Q) ⇔ (¬P ∨ ¬Q)
*)
Theorem demorgan_1: forall P Q : Prop, ~(P /\ Q) <-> (~P \/ ~Q).
Proof. intros p q. unfold iff. split.
- intros H. apply not_and_or in H. assumption.
- intros H. apply or_not_and in H. assumption. Qed.
@ikanher
ikanher / c-to-f-pytorch-gradient-descent-autograd.ipynb
Created July 2, 2018 17:57
Gradient descent bias convergence problem (convert celcius to f)
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.