(* The code of this file is a modified version of the axioms included with Autosubst 2 *)
Axiomatic Assumptions
For our development, we have to extend Coq with one well known axiomatic assumptions, namely functional extensionality.Functional Extensionality
We import the axiom from the Coq Standard Library and derive a utility tactic to make the assumption practically usable.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import Program.Tactics.
Tactic Notation "nointr" tactic(t) :=
let m := fresh "marker" in
pose (m := tt);
t; revert_until m; clear m.
Ltac fext := nointr repeat (
match goal with
[ |- ?x = ?y ] =>
(refine (@functional_extensionality_dep _ _ _ _ _) ||
refine (@forall_extensionality _ _ _ _) ||
refine (@forall_extensionalityP _ _ _ _) ||
refine (@forall_extensionalityS _ _ _ _)); intro
end).
Require Import Program.Tactics.
Tactic Notation "nointr" tactic(t) :=
let m := fresh "marker" in
pose (m := tt);
t; revert_until m; clear m.
Ltac fext := nointr repeat (
match goal with
[ |- ?x = ?y ] =>
(refine (@functional_extensionality_dep _ _ _ _ _) ||
refine (@forall_extensionality _ _ _ _) ||
refine (@forall_extensionalityP _ _ _ _) ||
refine (@forall_extensionalityS _ _ _ _)); intro
end).